8 papers
MechMath Agent Team: LLM Driven Agents for Mathematical Research
Yichuan Cao, Ruichen Qiu, Junqi Liu +5
AI reasoning has become a central focus in contemporary artificial intelligence, largely driven by the success of large language models. However, mathematical research, which is ch…
Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs
Beibei Xiong, Hangyu Lv, Junqi Liu +5
Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Sym…
Automated Tactics for Polynomial Reasoning in Lean 4
Hao Shen, Junyu Guo, Junqi Liu +1
Applying Gröbner basis theory to concrete problems in Lean 4 remains difficult since the current formalization of multivariate polynomials is based on a non-computable representat…
MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
Ruichen Qiu, Yichuan Cao, Junqi Liu +4
Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems that require c…
Formalizing Gröbner Basis Theory in Lean
Junyu Guo, Hao Shen, Junqi Liu +1
We present a formalization of Gröbner basis theory in Lean 4, built on top of Mathlib's infrastructure for multivariate polynomials and monomial orders. Our development covers the…
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
Junqi Liu, Zihao Zhou, Zekai Zhu +10
Agentic systems have recently become the dominant paradigm for formal theorem proving, achieving strong performance by coordinating multiple models and tools. However, existing app…