Automated conjecture resolution with formal verification

Large language models have made rapid progress in mathematical reasoning, yet reliably solving and verifying research-level problems remains challenging. Here we introduce an automated system that combines theorem retrieval, informal mathematical reasoning, and formal verification to solve and certify research-level mathematical problems end to end. The system couples Rethlas, an informal reasoning agent equipped with the mathematical theorem search engine Matlas, with Archon, a formalization agent equipped with LeanSearch. Using this framework, we resolve an open problem in commutative algebra posed by D.D. Anderson in 2014 and formally verify the resulting proof in Lean4. Additional research-level studies further illustrate the ability of Rethlas to support informal mathematical reasoning and discovery across several domains, and of Archon to formalize research-level proofs in Lean4. Our results illustrate a paradigm for mathematical research in which informal and formal reasoning systems, equipped with theorem-retrieval tools, operate in tandem to produce verifiable results and offer a concrete instantiation of human-AI collaborative mathematical research.