RESEARCH BRIEF
Can AI turn a difficult argument into a checkable proof?
Formalize and prove difficult mathematical problems in Lean, with machine-checked rigor at the core.
This HARD Lab direction studies the problem as an end-to-end system rather than as a single model demo. Current related work provides useful building blocks and baselines [1] [2] [3] [4] [5]; the lab’s goal is to connect them into measurable, reproducible research artifacts.
Formalizing mathematical statements and supporting definitions
AI-assisted lemma discovery and proof development
Lean-checked proof artifacts and reproducible evaluation
PROPOSED WORKFLOW
Build, measure, iterate.
Formalize
Translate the mathematical question into precise definitions and a theorem statement in Lean.
Develop proof
Explore intermediate lemmas and proof strategies, using AI to assist with candidate construction.
Check
Submit the formal proof to Lean for checking; distinguish a plausible argument from an accepted proof artifact.
STUDENT ENTRY POINTS
Ways to start contributing.
- Formalizing mathematical statements and supporting definitions
- AI-assisted lemma discovery and proof development
- Lean-checked proof artifacts and reproducible evaluation
RELATED WORK / 2026-09-10
Selected papers & citations.
Five primary-source papers selected to frame this direction. Links point to the authors’ arXiv records; these are external works, not HARD Lab publications.
5 selected papers · newest first by initial submission
Beyond Correctness: Toward Automated Novelty Verification with Lean 4
Discusses why a kernel-accepted proof and a mathematically novel result are different claims, and explores novelty verification.
Why it matters here. Useful as a recent caution about research evaluation. The author leaves large-scale quantitative evaluation to future work; this is not a validated novelty oracle.
Full citation & BibTeX
Ayrton Porto (2026). Beyond Correctness: Toward Automated Novelty Verification with Lean 4. arXiv:2608.14669. https://doi.org/10.48550/arXiv.2608.14669
@misc{hardlab_beyond_correctness,
title = {{Beyond Correctness: Toward Automated Novelty Verification with Lean 4}},
author = {Ayrton Porto},
year = {2026},
eprint = {2608.14669},
archivePrefix = {arXiv},
doi = {10.48550/arXiv.2608.14669},
url = {https://arxiv.org/abs/2608.14669},
note = {External related work; metadata checked 2026-09-10}
}Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
Studies augmented Lean formalisation and efficient formal-prover training.
Why it matters here. Informs data and compute-efficiency experiments. Independently check the validity of generated training statements and accepted proofs.
Full citation & BibTeX
Joshua Ong Jun Leang et al. (2026). Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation. arXiv:2606.12594. https://doi.org/10.48550/arXiv.2606.12594
@misc{hardlab_pythagoras,
title = {{Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation}},
author = {Joshua Ong Jun Leang and Zheng Zhao and Mihaela Cătălina Stoian and Qiyuan Xu and Haonan Li and Wenda Li and Shay B. Cohen and Eleonora Giunchiglia},
year = {2026},
eprint = {2606.12594},
archivePrefix = {arXiv},
doi = {10.48550/arXiv.2606.12594},
url = {https://arxiv.org/abs/2606.12594},
note = {External related work; metadata checked 2026-09-10}
}LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
Explores agentic formal mathematics using problem decomposition, informal plans, and interaction with a proof environment.
Why it matters here. A recent reference for coordinating proof attempts and using Lean feedback inside a tool-driven loop.
Full citation & BibTeX
Po-Nien Kung et al. (2026). LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks. arXiv:2606.03303. https://doi.org/10.48550/arXiv.2606.03303
@misc{hardlab_leap,
title = {{LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks}},
author = {Po-Nien Kung and Linfeng Song and Dawsen Hwang and Jinsung Yoon and Chun-Liang Li and Simone Severini and Mirek Olšák and Edward Lockhart and Quoc V Le and Burak Gokturk and Thang Luong and Tomas Pfister and Nanyun Peng},
year = {2026},
eprint = {2606.03303},
archivePrefix = {arXiv},
doi = {10.48550/arXiv.2606.03303},
url = {https://arxiv.org/abs/2606.03303},
note = {External related work; metadata checked 2026-09-10}
}DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
Uses subgoal decomposition and reinforcement learning to improve formal theorem proving.
Why it matters here. A model-level baseline to compare against retrieval, tool orchestration, and different proof-search budgets.
Full citation & BibTeX
Z.Z. Ren et al. (2025). DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. arXiv:2504.21801. https://doi.org/10.48550/arXiv.2504.21801
@misc{hardlab_deepseek_prover,
title = {{DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition}},
author = {Z.Z. Ren and Zhihong Shao and Junxiao Song and Huajian Xin and Haocheng Wang and Wanjia Zhao and Liyue Zhang and Zhe Fu and Qihao Zhu and Dejian Yang and Z.F. Wu and Zhibin Gou and Shirong Ma and Hongxuan Tang and Yuxuan Liu and Wenjun Gao and Daya Guo and Chong Ruan},
year = {2025},
eprint = {2504.21801},
archivePrefix = {arXiv},
doi = {10.48550/arXiv.2504.21801},
url = {https://arxiv.org/abs/2504.21801},
note = {External related work; metadata checked 2026-09-10}
}LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Provides a theorem-proving environment and datasets for retrieval-augmented language-model proving.
Why it matters here. A foundation for reproducible premise retrieval, proof-state interaction, and leakage-aware benchmark design.
Full citation & BibTeX
Kaiyu Yang et al. (2023). LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. arXiv:2306.15626. https://doi.org/10.48550/arXiv.2306.15626
@misc{hardlab_leandojo,
title = {{LeanDojo: Theorem Proving with Retrieval-Augmented Language Models}},
author = {Kaiyu Yang and Aidan M. Swope and Alex Gu and Rahul Chalamala and Peiyang Song and Shixing Yu and Saad Godil and Ryan Prenger and Anima Anandkumar},
year = {2023},
eprint = {2306.15626},
archivePrefix = {arXiv},
doi = {10.48550/arXiv.2306.15626},
url = {https://arxiv.org/abs/2306.15626},
note = {External related work; metadata checked 2026-09-10}
}No selected papers match this filter.