nLab coupling proof assistants with machine learning -- references

Coupling proof assistants with machine learning

On coupling proof assistants with machine learning:

• Li-An Yang et al, Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants [arXiv:1602.07455]

• Klaus Mainzer: From Proof Theory to Proof Assistants – Challenges of Responsible Software and AI, talk at Arbeitstagung Bern-München (2019) [pdf]

• Kaiyu Yang, Jia Deng: Learning to Prove Theorems via Interacting with Proof Assistants [arXiv:1905.09381]

• Cezary Kaliszyk: Machine Learning for Theorem Proving, lecture notes (2023) [pdf:1, 2, 3, 4, 5, 6]

• Garrett Mills: Adventures in AI-assisted proof generation (Mar 2023)

• NeurIPS 2023: Tutorial on Machine Learning for Theorem Proving (2023)

• Terence Tao: Machine-Assisted Proof, Notices of the AMS 72 1 (2024) [doi:10.1090/noti3041, pdf, full issue:pdf]

• Terence Tao: Machine-Assisted Proof, AMS Colloquium Lectures at the 2024 Joint Mathematics Meetings [video:YT]

• Peiyang Song, Kaiyu Yang, Anima Anandkumar: Towards Large Language Models as Copilots for Theorem Proving in Lean [arXiv:2404.12534]

• Leni Aniva et al.: Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 [arXiv:2410.16429]

• Kaiyu Yang et al.: Formal Mathematical Reasoning: A New Frontier in AI [arXiv:2412.16075]