LeanGraphSearch is a graph‑based retrieval method for the Lean 4 theorem prover that builds a dependency graph from Mathlib’s forward dependencies and traverses it to find supporting lemmas via multi‑hop chains. By linking each declaration to its premises, propagating relevance through a graph‑ranking algorithm, and re‑ranking candidates against the original query, it improves recall by up to 12% over LeanSearch v2 on MathlibQR and increases coverage of complete annotated proof routes on MathlibMPR by up to 3.7%. When integrated into an iterative proving loop, LeanGraphSearch raises pass rates at 8, 16, and 32 reflection turns by as much as 40% compared to a vanilla prover and up to 10% compared to LeanSearch v2, demonstrating higher accuracy‑cost efficiency.
By Yihan Xu, Jia-Chen Gu, Junyi Zhang, Di Wu, Haikang Deng, Po-Nien Kung, Kai-Wei Chang, Amit Sahai, Wei Wang, Nanyun Peng
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
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
arXiv:2606. 09450v1 Announce Type: new Abstract: LLMs have recently achieved strong results on formal proving benchmarks.
By QuocViet Pham, Elvir Karimov, Andrey Galichin, Ivan Oseledets
LLMs have recently achieved strong results on formal proving benchmarks. However, existing evaluations remain heavily concentrated on competition-style problems and often fail to capture how models behave on longer, more dependency-rich mathematical developments.
arXiv:2509. 03059v2 Announce Type: replace-cross Abstract: Recent advances in Large Language Models (LLMs) have shown that their reasoning capabilities can be significantly improved through Reinforcement Learning with Verifiable Reward (RLVR), particularly in domains like mathematics and programming, where ground-truth correctness can be automatically evaluated.
By Xingyue Huang, Rishabh, Gregor Franke, Ziyi Yang, Jiamu Bai, Weijie Bai, Jinhe Bi, Zifeng Ding, Yiqun Duan, Chengyu Fan, Wendong Fan, Xin Gao, Ruohao Guo, Yuan He, Zhuangzhuang He, Xianglong Hu, Neil Johnson, Bowen Li, Fangru Lin, Siyu Lin, Tong Liu, Yunpu Ma, Hao Shen, Hao Sun, Beibei Wang, Fangyijie Wang, Hao Wang, Haoran Wang, Yang Wang, Yifeng Wang, Zhaowei Wang, Ziyang Wang, Yifan Wu, Zikai Xiao, Chengxing Xie, Fan Yang, Junxiao Yang, Qianshuo Ye, Ziyu Ye, Guangtao Zeng, Yuwen Ebony Zhang, Zeyu Zhang, Zihao Zhu, Bernard Ghanem, Philip Torr, Guohao Li