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
Collector, NL Prover, and FL Prover coordinate across problem collection, informal reasoning, and formal proof.
View Agent TeamResearch Team
Researchers collaborating on AI-assisted mathematical discovery, proof development, and formal verification.
View All Team MembersPublications
- 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
Blogs
Research notes, project updates, and technical reflections on AI for Mathematics.
View Blogs