A team of researchers has built an AI system that solved 11 open mathematical problems in two months - not by brute-force search, but through a structured multi-agent architecture designed to handle the messy, non-linear way real math research actually works.
The MechMath Agent Team (MMAT) pairs three specialized agents - a Knowledge Base Manager, a Natural Language Prover, and a Formal Language Prover - in a closed loop. They run on top of what the researchers call a Harness Architecture, which splits system responsibilities into control, execution, and augmentation layers. The idea is to let the system handle open-ended exploration without losing the logical rigor that mathematical proof demands. Problems tested spanned Number Theory, Algebraic Complexity Theory, Differential Algebra, Operator Algebra, and Inequalities.
Most AI math benchmarks measure performance on problems with known answers. MMAT was pointed at genuinely unsolved problems, which is a harder and more meaningful test. If the formal proofs hold up to scrutiny, 11 verified results in two months would represent a meaningful contribution to the literature - not a benchmark score, but actual mathematics.
The results are still self-reported in a preprint, and independent verification of the proofs will matter. The broader pattern, though, is notable: formal proof assistants like Lean and Coq have been creeping toward AI integration for years, and systems like MMAT represent a more aggressive push to close that loop. Whether this scales beyond the problems the team chose to test it on is the question worth watching.