FaithSieve is a Lean‑assisted framework that fine‑grains natural‑language mathematical proofs into local reasoning units, extracts typed proof obligations, and verifies them with formal evidence gated by semantic alignment. It introduces two expert‑verified datasets—ProofLoc‑Olympiad and ProofLoc‑University—to benchmark first‑error localization. On these benchmarks, FaithSieve outperforms direct‑judging baselines, achieving 81.43% and 84.5% exact first‑error accuracy respectively.
By Ziyu Wang, Qiming Dai, Yishan Wu, Zaiwen Wen
arXiv:2505. 18492v5 Announce Type: replace Abstract: Mathematical competition problems fall into two broad types: theorem proving, which asks for a proof of a given statement, and answer construction, which requires constructing a property-satifying object with proofs.
By Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel
RePro is a framework that rewrites benchmark problems for large language models (LLMs) in mathematical problem solving, ensuring that the rewritten problems and their answers are valid and correct through Lean-verified proofs. It integrates Lean-oriented neural automated theorem provers (ATPs) to regenerate answers, achieving 100% well-definedness, feasibility, and answer correctness on GSM8K and MATH datasets. Experiments show that models’ performance drops on these proof‑verified rewritten benchmarks, indicating sensitivity to surface‑level and structural variations and potential memorization effects.
By Xiyuan Zhou, Zhuoqi Li, Xinlei Wang, Yirui He, Yuhao Wu, Yuheng Cheng, Yan Xu, Junhua Zhao, Jinjin Gu
arXiv:2608. 14221v1 Announce Type: new Abstract: Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4.
By Lushi Pu, Weiming Zhang, Xinheng Xie, Zixuan Fu, Bingxiang He, Hengyu Zhao, Hongya Lyu, Xin Li, Jie Zhou, Yudong Wang
arXiv:2606. 12594v1 Announce Type: new Abstract: Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both supervised fine-tuning (SFT) and sampling expensive.
By Joshua Ong Jun Leang, Zheng Zhao, Mihaela C\u{a}t\u{a}lina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia
The paper introduces TopoAlign, a framework that repurposes code repositories to train Math LLMs by decomposing code into docstrings, main functions, and dependency functions and reassembling them into structures that mirror formal mathematical statements. Using this approach, the authors train three state‑of‑the‑art models—DeepSeek‑Math, Qwen‑3, and Herald—and evaluate them on MiniF2F, Putnam, and ProofNet benchmarks. TopoAlign yields significant performance gains, notably a 17.77% improvement on BEq@10 and a 68.82% boost on typecheck@10 for DeepSeek‑Math, while also providing modest gains for Herald.
By Yupei Li, Philipp Borchert, Gerasimos Lampouras
arXiv:2609.35790v1 Announce Type: cross
Abstract: While neural theorem provers have achieved impressive milestones in formal mathematics, they largely operate on the assumption that faithful Lean 4 f...
By Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wengping Deng, Liang Zhang
arXiv:2606. 15258v1 Announce Type: new Abstract: Large language models (LLMs) are increasingly capable of mathematical problem solving and can even assist with research-level proofs, yet we still lack a scalable and reproducible way to measure step-level reasoning in long proofs across diverse sources.
By Jierui Zhang, Siyuan Tan, Xinhang Li, Longzhuangzhi Lin, Dailin Li, Chengfeng Gu, Xinping Li, Yaxian Hao, Shengjia Liang, Yuxiang Ren, Wenhao Liu
arXiv:2605. 19723v2 Announce Type: replace-cross Abstract: Mathematical reasoning is essential for problem-solving in education, science, and industry, serving as a crucial benchmark for evaluating artificial intelligence systems.
By Husnain Amjad, Raja Khurram Shahzad, Aamir Shahzad, Mehwish Fatima
Magenta is a training‑free pipeline that bridges informal natural‑language mathematical problems and formal Lean 4 verification. Given a problem in plain text, it generates an answer, translates it into a Lean 4 statement, and constructs a machine‑checked proof. The system includes a statement judge to ensure the formalisation matches the original problem and an error‑attribution judge to guide corrections, achieving perfect accuracy on olympiad benchmarks and solving all six IMO 2026 problems when combined with K2‑Horizon‑7B.
By Joshua Ong Jun Leang, Haonan Li, Zheng Zhao, Xinyi Shang, Wenda Li, Zhengzhong Liu, Erix Xing, Shay Cohen, Eleonora Giunchiglia
arXiv:2607. 11307v1 Announce Type: new Abstract: Full-proof autoformalization bridges extensive mathematical proofs in natural language with formally validated reasoning, offering a pathway to elevate the ceiling of verifiable mathematical reasoning.
By Tian-Shuo Liu, Shiyuan Zhang, Zijie Geng, Haoyu Liu, Runjie Xu, Pengyuan Wang, Lei Yuan, Yang Yu
ReSolve is a training‑free inference method that reuses candidate reasoning by selectively moderating generative outputs. It examines existing derivations when candidates disagree or lack a parseable answer, then incorporates new solutions into a bounded loop. On 130 competition‑mathematics problems, ReSolve achieves 100 and 99 correct answers with significantly fewer tokens than eight‑sample self‑consistency, while a controlled ablation shows that visible derivations improve accuracy.
By Bangji Yang, Jiajun Fan, Hongba Ma, Xi Zhu, Weizhi Zhang, Minghao Guo, Ye Li, Hamid Palangi, Jiaxuan You