Research notes, project updates, and technical reflections on AI for mathematics. Each post connects mathematical ideas with the systems, proof artifacts, and research practices behind them.
As AI systems become increasingly capable at mathematical reasoning, the central question is no longer whether mathematicians should use them, but how. Xiao-Shan Gao explains how mathematical research agents combine language models, formal verification, and persistent knowledge—and why human creativity must remain in the lead.
MechGeo unifies autoformalization and automated proving for trustworthy Euclidean geometry. It produced Lean-checked statements, proofs, and counterexamples for 44 IMO geometry problems from 2000–2026 and achieved faithful coverage of all 14 LEAP geometry problems after validation and repair.
The MechMath Agent Team project template is now publicly available. Learn how to create a research project, install its dependencies, and launch its natural-language, formal-language, and knowledge-management agents.
A progress report on complete natural-language and Lean 4 solutions to all six IMO 2026 problems. It presents the public proof artifacts, verification workflow, and recorded NL/FL proof-generation times.
A review of automated theorem proving from Hilbert’s decision problem to LLM-based research agents, with an introduction to MechMath Agent Team. It traces the shift from symbolic automation and interactive proving to agent systems that support mathematical research.
No blogs match your search.