MechMath
Key Lab of Mathematics Mechanization
About MechMath
MechMath is a research initiative of the Key Laboratory of Mathematics Mechanization, AMSS, CAS. We bring together mathematicians, computer algebra, formal verification, and AI to build systems for mathematical research and to develop rigorous new results. Our work spans AI-assisted discovery, theorem proving in natural language and Lean, symbolic computation, and the publication of reusable mathematical artifacts.
MechMath Systems
MechMath develops AI systems that help mathematicians organize knowledge, explore conjectures, construct proofs, and verify results.
Explore SystemsResearch Team
Xiao-Shan Gao
Lihong Zhi
Ruyong Feng
Dakai Guo
Yichuan Cao
Junqi Liu
Yunfei Li
Ruichen Qiu
Hao Shen
Blogs
- MechGeo: Automatically Formalizing and Proving IMO Geometry in Lean 4 MechMath Team
- MechMath Agent Team Is Now Open Source MechMath Team
- IMO 2026: From Natural-Language Solutions to Lean Verification MechMath Team
- From Hilbert's Decision Problem to Reasoning Agents Xiao-Shan Gao
Publications
- MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4 Hao Shen, Junyu Guo, Tian Cui, Yuxuan Xiao, Lihong Zhi
- MechMath Agent Team: LLM Driven Agents for Mathematical Research Yichuan Cao, Ruichen Qiu, Junqi Liu, Jiaqi Wang, Dakai Guo, Ruyong Feng, Lihong Zhi, Xiao-Shan Gao
- Deterministic Polynomial-time Exact-root Computation for Sparse Polynomials with Bounded Total Degree Qiao-Long Huang, Yichuan Cao, Ruichen Qiu, Xiao-Shan Gao
- The Equivalence Problem for Generalized Airy Operators Yichuan Cao, Ruyong Feng, Yunfei Li, Ruichen Qiu
- Complexity of Low-Degree Skew Polynomial Multiplication over Finite Fields Ke Ye, Yichuan Cao, Ruichen Qiu
- MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving Ruichen Qiu, Yichuan Cao, Junqi Liu, Dakai Guo, Xiao-Shan Gao, Lihong Zhi, Ruyong Feng
- Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number Yichuan Cao, Dakai Guo, Ruichen Qiu, Ruyong Feng, Xiao-Shan Gao