Formal Verification & Neural Theorem Proving Reading List

Curated by Mouhssine Rifaki | Stanford Electrical Engineering | Last updated August 2026

Neural theorem proving brings language models into formal mathematics. This list spans premise selection, whole-proof generation, and Lean-based environments that make verification learnable.

Formal Verification & Neural Theorem Proving: 10 key papers

1. Generative Language Modeling for Automated Theorem Proving
   Polu and Sutskever. arXiv 2020.
2. HyperTree Proof Search for Neural Theorem Proving
   Lample et al. arXiv 2022.
3. Proof Artifact Co-training for Theorem Proving with Language Models
   Han et al. arXiv 2021.
4. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
   Yang et al. arXiv 2023.
5. Baldur: Whole-Proof Generation and Repair with Large Language Models
   First et al. arXiv 2023.
6. DeepMath - Deep Sequence Models for Premise Selection
   Alemi et al. arXiv 2016.
7. Learning to Prove Theorems by Learning to Generate Theorems
   Wang and Deng. arXiv 2020.
8. Formal Mathematics Statement Curriculum Learning
   Polu et al. arXiv 2022.
9. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
   Jiang et al. arXiv 2022.
10. GamePad: A Learning Environment for Theorem Proving
    Huang et al. arXiv 2018.

Related reading lists

• Retrieval-Augmented Generation
• Curriculum Learning & Teacher-Student
• Chain-of-Thought & Reasoning
• Code Generation & Program Synthesis with RL
• Certified Robustness
• Preference Learning & Learning from Comparisons
• Prompt Optimization & In-Context Learning for LLMs
• Neural Operators & PDE Solvers