The paper introduces DAPS, a dependency‑aware premise selector for large language model theorem proving in Lean 4. By curating underused dependency resources from 53 Lean Blueprint projects and extracting typed, multi‑level Mathlib4 dependencies, DAPS employs a structural neighborhood encoder and a group‑level contrastive objective to overcome frequency skew, isolated ranking, and out‑of‑distribution degradation. It achieves a mean Recall@32 of 89.25 on Mathlib4‑Heldout, outperforming the strong selector LeanHammer, and improves theorem proving on miniF2F and IMO‑ProofBench.
By Zixuan Chen, Wenyuan Jiang, Junling Wang, Mrinmaya Sachan, Yinya Huang
MathAdv is a diagnostic benchmark for formal theorem proving that covers 13 undergraduate- and graduate-level mathematics domains. It includes Lean 4 proofs and up to three auxiliary tasks—multiple-choice questions, fill-in-the-blank problems, and expert-crafted transformations—to probe knowledge, informal reasoning, and robustness to problem presentation. Evaluation of current theorem provers shows formalization is a major bottleneck, performance varies by domain, natural-language guidance can help or hinder models, and equivalent reformulations reveal significant robustness gaps.
By Jiaxin Yuan, Connor Martinez Lockhart, Xiaoyu Liu, Jiaqi Wang, Chenghao Deng, Xiayimei Han, Vlasios Mastrantonis, Dmitrii Gudin, Shaopeng Zhu, Abdirisak Abdullahi Mohamed, Bilal Hamdi Aytekin, Jiewen Lang, Zezheng Song, Furong Huang
The paper introduces a method for evaluating the intrinsic interestingness of mathematical theorems by comparing the length of their proofs to the length of their statements. It trains a 27B language model to predict proof difficulty, enabling the generation and selection of more interesting theorems while significantly reducing overlap with existing Mathlib. The approach allows iterative expansion of a self‑building, machine‑verified mathematical library guided by quantifiable metrics.
By Niket Patel, Ahmad Rammal, Amaury Hayat, Remi Munos, Julia Kempe
Large language models (LLMs) have achieved remarkable performance on high-school and olympiad-style mathematics, yet their capabilities on advanced mathematics remain poorly understood. Existing benchmarks, however, fall short in both scope and evaluation granularity: they provide limited disciplinary coverage and often rely on final-answer correctness or coarse judgments, leaving the validity of the reasoning process inadequately assessed.
The paper argues that large language models (LLMs) organize their internal mathematical reasoning by reusable reasoning approaches rather than by the benchmark topics they are tested on. Using a generation‑replay protocol, the authors extract activation‑importance signatures from eight models across five math sources, cluster these signatures, and find that the resulting groups align more closely with reasoning approaches than with topics. The study shows that changing the requested reasoning approach shifts cluster assignments, while paraphrasing the prompt does not, underscoring the primacy of approach over topic in LLM reasoning.
By Sajad Goudarzi, Samaneh Zamanifard, Moloud Nasiri, Hamed Rahimian
arXiv:2610. 02191v1 Announce Type: new Abstract: While Large Language Models (LLMs) have demonstrated striking capabilities on frontier mathematical problems, it remains unclear whether they possess the structural mathematical understanding underlying their solutions.
By Shuo Xing, Zilin Dai, Chengyuan Qian, Fangzhou Lin, Wenjing Chen, Ping He, Pan Lu, Alvaro Velasquez, Mohit Bansal, Zhengzhong Tu
arXiv:2606. 16206v1 Announce Type: new Abstract: Large language models are increasingly proposed as educational tutors, yet stronger task-solving ability does not necessarily imply stronger learning support.
By Junyi Yao, Zihao Zheng, Baichuan Li
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:2606.16206v2 Announce Type: replace
Abstract: Large language models are increasingly proposed as educational tutors, yet stronger task-solving ability does not necessarily imply stronger learni...
By Junyi Yao, Zihao Zheng, Baichuan Li
The paper introduces a source‑grounded framework that represents mathematical arguments as directed acyclic graphs, incorporating numbered and unnumbered statements, equations, assumptions, and constructions while distinguishing source occurrences from contextual states and inference records. It defines measurement metrics such as depth (longest prerequisite path) and bulk (distinct ancestor edges), and provides a standardized, versioned prompt protocol for annotation discovery, deterministic recomputation, and review assistance. The framework also supports cross‑paper links to explore theorem co‑use, rare combinations, and dependency communities, aiming to motivate probabilistic premise suggestions and review of omissions or unchecked conditions in both human‑written and AI‑generated proofs.
The paper introduces a framework that uses large language models to represent and measure mathematical arguments, capturing statements, equations, assumptions, and constructions while distinguishing source occurrences from contextual states and inference records. It defines a directed acyclic graph representation where depth is the longest prerequisite path and bulk counts distinct ancestor edges, providing a recurrence that handles shared subarguments and preserves macro skeletons. The framework includes a standardized, versioned prompt protocol for annotation discovery, deterministic recomputation, and review assistance, and proposes cross‑paper links to study theorem co‑use and support probabilistic premise suggestions and review of omissions.
By Eunji Park
AdvancedMathBench is a new benchmark suite that evaluates large language models on advanced mathematical proof generation and verification. It includes ProverBench, with 245 problems from undergraduate to doctoral qualifying‑exam levels, and VerifierBench, which tests models’ ability to judge proof validity using 888 expert‑annotated trajectories. The suite features an automatic verification pipeline trained on expert data, and results show that even state‑of‑the‑art models perform poorly, highlighting a gap between generation and verification skills.
By Lingkai Kong, Zijian Wu, Yuzhe Gu, Haiteng Zhao, Zhouqi Hua, Wenyong Huang, Shuang Sun, Zhicheng Xiong, Xiaotian Zhang, Shuya Zhao, Yan Wang, Disheng Xu, Wenwei Zhang, Kai Chen