9 papers
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…
Tangent classes of matroids and wonderful compactifications
Ronnie Cheng, Shurui Liu, Guoxiong Gao
For every loopless matroid and every Feichtner--Yuzvinsky building set containing the top flat, we construct an integral tangent class $T_{M,\mathcal{G}}^{\mathbb…
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…
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…
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…
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…