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
- IMO 2026: From Natural-Language Solutions to Lean Verification MechMath Team
- From Hilbert's Decision Problem to Reasoning Agents Xiao-Shan Gao
Publications
- 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
- A Greatest Common Divisor Criterion of Certain Binomial Coefficients Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng, Xiao-Shan Gao