MechMath
Key Lab of Mathematics Mechanization
About MechMath
MechMath Agent Team (MMAT) is a large language model driven agent designed as a co-pilot throughout the full cycle of mathematical research, including organizing and utilizing mathematical knowledge, proving theorems in natural language, proving theorems in formal language using Lean, proposing new conjectures, and drafting research papers in LaTeX.
MechMath Agent Team
Knowledge Base Manager (KB-Manager)，Natural Language Prover (NL-Prover)，Formal Language Prover (KL-Prover) coordinate across mathematical problems.
View Agent TeamResearch Team
Xiao-Shan Gao
Lihong Zhi
Ruyong Feng
Dakai Guo
Jiaqi Wang
Junqi Liu
Ruichen Qiu
Yichuan Cao
Blogs
Research notes, project updates, and technical reflections on AI for Mathematics.
View BlogsPublications
- Output-sensitive Sparse Polynomial GCD over Finite Fields is NP-hard Ruichen Qiu, Yichuan Cao, Qiao-Long Huang, Ruyong Feng, Xiao-Shan Gao
- Sparse Polynomial Divisibility Test over Finite Field is CoNP-hard Yichuan Cao, Ruichen Qiu, Qiao-Long Huang, Ruyong Feng, Xiao-Shan Gao
- Quasi-linear Time Multiplication of Sparse Polynomials with Integer Coefficients Qiao-Long Huang, Yichuan Cao, Ruichen Qiu, Xiao-Shan Gao
- A Finite Certificate for the Positive $n=9$ Vasc Inequality Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng