KB-Manager, NL-Prover, and FL-Prover operate as a closed loop that accumulates mathematical knowledge, develops proofs, and produces formal certification.
MMAT is organized as a closed loop of three domain-specialized agents: the KB-Manager maintains a shared, auditable memory graph; the NL-Prover orchestrates exploration and synthesizes natural-language proofs; and the FL-Prover formalizes and mechanically verifies these derivations in Lean 4. Select an agent portrait to explore its role, relationships with the rest of the team, and the capabilities it coordinates.
NL-Prover
Leads mathematical discovery by coordinating a scalable proof pipeline that synthesizes and revises natural-language proofs.
Subagents
Coordinates core derivation, grounded interfaces, advanced reasoning, and documentation agents for decomposition, recovery, auditing, and publication-ready synthesis.
Tools & infrastructure
Its command-line tooling handles literature retrieval, PDF parsing, programmatic execution, and structural schema gating so the agents can focus on logical synthesis.
Knowledge Base
The KB-Manager turns the team's sources, proof fragments, formal artifacts, and verified obstructions into a shared mathematical dependency and evidence graph.
A project-scoped memory graph preserves reusable results and the reasoning paths that produced them.
Full-Cycle Theorem Proving
Using OEIS A287616 as a case study, MMAT coordinates 137 specialized subagents through mathematical exploration, computational certification, and iterative Lean 4 verification. The resulting proof comprises more than 3,500 lines of formally checked Lean code. Select a stage card to examine the corresponding work in detail.
Project-Level Discovery
Starting from one sparse-polynomial multiplication problem, MMAT expanded the investigation into six connected research directions. Select a theme to trace the question it inherited and the result it produced.
MMAT settled the problem over the integers after auditing the proof chain, finding a counterexample to a flawed argument, and reconstructing a verified proof.
Divisibility
Prior Work
Plaisted (1984) posed the complexity question for sparse polynomial divisibility testing.
MMAT Result
Over finite fields, MMAT established that sparse polynomial divisibility testing is coNP-hard under BPP reductions.
Roots
Prior Work
Bi et al. (2016) showed that deciding whether a sparse polynomial has a finite-field root is NP-hard.
MMAT Result
MMAT showed that deciding whether a sparse polynomial vanishes at a root of unity is NP-hard.
GCD
Prior Work
Davenport et al. (2009) asked whether output-sensitive sparse GCD computation is polynomial-time.
MMAT Result
MMAT resolved the finite-field problem by demonstrating output-sensitive GCD computation is NP-hard under BPP reductions.
Decomposition
Prior Work
Erdos conjectured that sparsity of h(x)^2 implies sparsity of h(x), later resolved in the univariate setting.
MMAT Result
MMAT solved the multivariate extension: sparsity of g^e implies sparsity of g, with a polynomial-time algorithm for g.
Factorization
Prior Work
Gathen and collaborators studied how the sparsity of factors is controlled by a sparse polynomial.
MMAT Result
MMAT proved that sparsity of gh implies sparsity of g and h when h is multilinear.
