18 papers
An AI-Assisted Formalization of the Poincaré Conjecture
Zhiyuan Zhang, Axel Delaval, Leheng Chen +6
We present an AI-assisted Lean 4 formalization of the Poincaré conjecture. The project began with limited reusable formal infrastructure for the geometric analysis behind the proof…
Constructing Rational Curves via Jets on Projective Varieties with Non-Nef Canonical Bundle
Bin Dong, Guoxiong Gao, Bin Guo +3
We give an algebraic proof in characteristic zero of the Miyaoka--Mori criterion: every point of a curve of negative canonical degree on a smooth projective variety lies on a ratio…
Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory
Jihao Liu, Guoxiong Gao, Zeming Sun +8
Recent LLM-based mathematical reasoning agents have begun to tackle research-level problems and, in several cases, have contributed to the resolution of open problems. However, sca…
From Search to Synthesis: Training LLMs as Zero-Shot Workflow Generators
Gan Luo, Zihan Qin, Bin Dong +1
Large language models (LLMs) excel across a wide range of tasks, yet their instance-specific solutions often lack the structural consistency needed for reliable deployment. Workflo…
Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning
Ruoran Xu, Haoyu Cheng, Bin Dong +1
Geometric problem solving, as a typical multimodal reasoning problem, has attracted much attention and made great progress recently, however most of works focus on plane geometry w…
Automated Conjecture Resolution with Formal Verification
Haocheng Ju, Guoxiong Gao, Jiedong Jiang +13
Recent advances in large language models have significantly improved their ability to perform mathematical reasoning, extending from elementary problem solving to increasingly capa…
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
Guoxiong Gao, Zeming Sun, Jiedong Jiang +5
Proving theorems in Lean 4 often requires identifying a scattered set of library lemmas whose joint use enables a concise proof -- a task we call global premise retrieval. Existing…
Matlas: A Semantic Search Engine for Mathematics
Haocheng Ju, Leheng Chen, Peihao Wu +2
Retrieving mathematical knowledge is a central task in both human-driven research, such as determining whether a result already exists, finding related results, and identifying his…
AI for Mathematics: Progress, Challenges, and Prospects
Haocheng Ju, Bin Dong
AI for Mathematics (AI4Math) has emerged as a distinct field that leverages machine learning to navigate mathematical landscapes historically intractable for early symbolic systems…
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…
Herald: A Natural Language Annotated Lean 4 Dataset
Guoxiong Gao, Yutong Wang, Jiedong Jiang +4
Verifiable formal languages like Lean have profoundly impacted mathematical reasoning, particularly through the use of large language models (LLMs) for automated reasoning. A signi…
A Semantic Search Engine for Mathlib4
Guoxiong Gao, Haocheng Ju, Jiedong Jiang +2
The interactive theorem prover Lean enables the verification of formal mathematical proofs and is backed by an expanding community. Central to this ecosystem is its mathematical li…