6 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…
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…
On some open problems in commutative algebra resolved by Rethlas
Jiedong Jiang, Yixiao Li, Zeming Sun +3
We report on a collection of open problems in commutative algebra and related areas that have been resolved (proved or disproved) using the Rethlas natural-language automated reaso…
Optimal bend-and-break for foliations
Jihao Liu, Zeming Sun, Jiedong Jiang
We show that for every foliation of rank on a normal projective variety, the optimal constant in the bend-and-break inequality for tangent rational curves is $r+1…
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…
The Absolute Anabelian Geometry of Virtual Curves Arising from Sections of Arithmetic Fundamental Groups of Configuration Spaces
Zeming Sun
The objective of this paper is to study the anabelian object referred to as \emph{pointed virtual curves}. Namely, given a family of curves over a field under…