Converting informal math language to Lean

Stream: general

[Notification Bot]

Daniel Donnelly has marked this topic as unresolved.

[Julian Berman]

@Jason Rute of the resources you mentioned any chance you have a single one you'd recommend as a good overview if I wasn't going to read all of them?

[Jason Rute]

@Julian Berman I found Szegedy's recorded talk at AITP 2020 interesting (and it gives a good discussion of the challenges with trying to align arXiv and theorem provers), but I think the best (and only to my knowledge) published results are by Wang et al and their newest results are here: https://arxiv.org/pdf/1912.02636.pdf.

[Julian Berman]

Fantastic, thanks!