7 papers · 1 filter
Translating Informal Proofs into Formal Proofs Using a Chain of States
Ziyu Wang, Bowen Yang, Chenyi Li +4
We address the problem of translating informal mathematical proofs expressed in natural language into formal proofs in Lean4 under a constrained computational budget. Our approach…
FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
Jiedong Jiang, Wanyi He, Yuefeng Wang +8
Recent advances in large language models (LLMs) have demonstrated impressive capabilities in formal theorem proving, particularly on contest-based mathematical benchmarks like the…
Aligning Perception, Reasoning, Modeling and Interaction: A Survey on Physical AI
Kun Xiang, Terry Jingchen Zhang, Yinya Huang +13
The rapid advancement of embodied intelligence and world models has intensified efforts to integrate physical laws into AI systems, yet physical perception and symbolic physics rea…
Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
Hanyu Wang, Ruohan Xie, Yutong Wang +3
Accurate auto-formalization of theorem statements is essential for advancing automated discovery and verification of research-level mathematics, yet remains a major bottleneck for…
Connected Theorems: A Graph-Based Approach to Evaluating Mathematical Results
Gergely Bérczi, Bin Dong, Haocheng Ju +1
The evaluation of mathematical results plays a central role in assessing researchers' contributions and shaping the direction of the field. Currently, such evaluations rely primari…
MIRB: Mathematical Information Retrieval Benchmark
Haocheng Ju, Bin Dong
Mathematical Information Retrieval (MIR) is the task of retrieving information from mathematical documents and plays a key role in various applications, including theorem search in…
REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
Ziju Shen, Naohao Huang, Fanyi Yang +11
Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this pa…