# Automated Conjecture Resolution with Formal Verification arXiv: https://arxiv.org/abs/2604.03789 ยท HTML: https://mlsanity.com/paper/2604.03789/ ## Key facts - Cited by 28 papers in the map (data through 14 Oct 2026). - Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. - Builds on 19 of its 40 references that are in the map. - First posted on arXiv 4 Apr 2026. ## Placed in - LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/) ## Builds on (most cited first, 19 of 19) - [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023) - [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025) - [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025) - [Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities](https://mlsanity.com/paper/2507.06261/) (2025) - [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024) - [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025) - [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024) - [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025) - [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026) - [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025) - [Towards Autonomous Mathematics Research](https://mlsanity.com/paper/2602.10177/) (2026) - [Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the ErdHos Problems](https://mlsanity.com/paper/2601.22401/) (2026) - [First Proof](https://mlsanity.com/paper/2602.05192/) (2026) - [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024) - [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025) - [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025) - [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025) - [Aletheia tackles FirstProof autonomously](https://mlsanity.com/paper/2602.21201/) (2026) - [Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium](https://mlsanity.com/paper/2603.15929/) (2026) ## Built on by (most cited first, 28 of 28) - [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026) - [Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory](https://mlsanity.com/paper/2607.06447/) (2026) - [ProofCouncil: An LLM Agent for Solving Open Mathematical Problems](https://mlsanity.com/paper/2607.09474/) (2026) - [Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration](https://mlsanity.com/paper/2607.27705/) (2026) - [Matlas: A Semantic Search Engine for Mathematics](https://mlsanity.com/paper/2604.17484/) (2026) - [Iteris: Agentic Research Loops for Computational Mathematics](https://mlsanity.com/paper/2606.02484/) (2026) - [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026) - [The Problem Is the Problem: Towards Scalable Mathematical Discovery](https://mlsanity.com/paper/2608.16977/) (2026) - [Evaluating Research-Level Math Proofs via Strict Step-Level Verification](https://mlsanity.com/paper/2606.10799/) (2026) - [SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematics](https://mlsanity.com/paper/2606.29894/) (2026) - [ReasFlow: Assisting Reasoning-Centric Scientific Discovery in Applied Mathematics via a Knowledge-Based Multi-Agent System](https://mlsanity.com/paper/2607.14178/) (2026) - [MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research](https://mlsanity.com/paper/2607.14582/) (2026) - [AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language](https://mlsanity.com/paper/2607.16372/) (2026) - [FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving](https://mlsanity.com/paper/2608.25220/) (2026) - [Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science](https://mlsanity.com/paper/2609.15983/) (2026) - [Grokability in five inequalities](https://mlsanity.com/paper/2605.05193/) (2026) - [Tangent classes of matroids and wonderful compactifications](https://mlsanity.com/paper/2607.05835/) (2026) - [Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory](https://mlsanity.com/paper/2607.17388/) (2026) - [Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research](https://mlsanity.com/paper/2608.15052/) (2026) - [EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discovery](https://mlsanity.com/paper/2609.00032/) (2026) - [Choir: An Open Protocol for Distributed Multi-Agent Autoformalization](https://mlsanity.com/paper/2609.31903/) (2026) - [ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization](https://mlsanity.com/paper/2609.34960/) (2026) - [GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research](https://mlsanity.com/paper/2609.36663/) (2026) - [Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization](https://mlsanity.com/paper/2609.39228/) (2026) - [Continual Graph Memory for Mathematical Research Agents](https://mlsanity.com/paper/2610.02945/) (2026) - [An AI-Assisted Formalization of the Poincar'e Conjecture](https://mlsanity.com/paper/2610.08329/) (2026) - [One-Sided Verification Under Limited Expert Review](https://mlsanity.com/paper/2610.18089/) (2026) - [Euler: Towards Human-Centered Multi-Agent Mathematical Discovery](https://mlsanity.com/paper/2610.19864/) (2026) ## Abstract (arXiv) Recent advances in large language models have significantly improved their ability to perform mathematical reasoning, extending from elementary problem solving to increasingly capable performance on research-level problems. However, reliably solving and verifying such problems remains challenging due to the inherent ambiguity of natural language reasoning. In this paper, we propose an automated framework that integrates natural language reasoning with formal verification to tackle research-level mathematical problems. Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon. Rethlas combines reasoning primitives with our theorem search engine, Matlas, to explore solution strategies and construct candidate proofs. Archon, equipped with LeanSearch, translates informal arguments into formalized Lean 4 projects through task decomposition, iterative refinement, and automated proof synthesis, ensuring machine-checkable correctness. Using this framework, we resolve an open problem in commutative algebra and formally verify the resulting proof in Lean 4 with essentially no human involvement. Additional case studies illustrate the capabilities of Rethlas in informal mathematical reasoning and discovery, as well as the ability of Archon to formalize research-level proofs in Lean 4. Our experiments demonstrate that strong theorem retrieval tools enable the discovery and application of cross-domain mathematical techniques, while the formal agent can autonomously fill nontrivial gaps in informal arguments. More broadly, our work illustrates a promising paradigm for mathematical research in which informal and formal reasoning systems, equipped with theorem retrieval tools, operate in tandem to produce verifiable results, reduce human effort, and support human-AI collaborative mathematical research.