PaperlayerView exact revision on arXiv

Source-linked AI summary

Automated Conjecture Resolution with Formal Verification

Haocheng Ju, Guoxiong Gao, Jiedong Jiang, Bin Wu, Zeming Sun, Shurui Liu, Leheng Chen, Yutong Wang, Yuefeng Wang, Zichen Wang, Wanyi He, Peihao Wu, Liang Xiao, Ruochuan Liu, Bryan Dai, Bin Dong

arXiv:2604.03789v2cs.LGcs.AI

TL;DR

The paper addresses the difficulty of reliably solving and verifying research-level mathematics expressed in ambiguous natural language. It combines the informal reasoning agent Rethlas with the formalization agent Archon, and demonstrates the framework by resolving and formally verifying an open commutative-algebra problem with essentially no human intervention.

  • Problem

    Research-level mathematical arguments remain difficult to verify reliably because natural-language reasoning is imprecise, even when assessed by experts.

  • Method

    Rethlas explores and constructs candidate proofs with theorem retrieval, while Archon decomposes and formalizes them into Lean 4 projects using LeanSearch and iterative refinement.

  • Results

    The framework resolved an open commutative-algebra problem and formally verified its proof in Lean 4 with essentially no human intervention, while additional cases demonstrated separate agent capabilities.

  • Takeaways & Limitations

    Informal and formal agents can cooperate on a genuine open mathematical problem, with the formal agent filling missing details and human involvement limited primarily to semantic verification.

  • Takeaways & Limitations

    Archon’s effectiveness depends on case-by-case guidance from a human formalization expert about which proof route is most tractable in the available Mathlib infrastructure.

Abstract

from arXiv · show

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.

1 Introduction

The paper motivates a framework combining informal mathematical reasoning with formal verification to address the difficulty of reliably evaluating and checking research-level proofs. It introduces Rethlas and Archon and reports an automated resolution of an open commutative-algebra problem with essentially no human intervention.

  • Research-level mathematical reasoning remains difficult to evaluate reliably because natural-language arguments are imprecise and can contain subtle errors.The paper argues that even expert review can occasionally misjudge mathematical arguments.
  • The proposed framework combines Rethlas, an informal reasoning agent with theorem retrieval, and Archon, a formalization agent using LeanSearch to produce verified Lean 4 projects.Archon uses structured planning, iterative formalization, and persistent memory management.
  • The framework automatically resolves Anderson’s 2014 open problem in commutative algebra and formally verifies the resulting proof in Lean 4 with essentially no human intervention.Matlas helps Rethlas discover Jensen’s key technical result, while Archon fills non-trivial gaps during formalization.
  • Additional case studies evaluate Rethlas on an unrecorded algebraic-groups problem and a p-adic Hodge theory problem, while separately demonstrating the agents’ research-level capabilities.The algebraic-groups case contrasts Rethlas’s successful proof with an incorrect proof from GPT-5.5 Pro.

2 Related Work

Related work shows strong progress in autonomous mathematical reasoning and Lean formalization, spanning olympiad benchmarks, research problems, and open conjectures. Existing systems vary substantially in their degree of autonomy and human collaboration.

  • Structured verification-and-refinement systems have solved 5 out of 6 IMO 2025 problems, surpassing the models’ baseline performance without such workflows.
  • Aletheia has autonomously tackled four Erdős problems and addressed additional research questions, while also working semi-autonomously with human collaboration.
  • Lean-oriented systems have achieved strong competition results, including silver-medal performance at IMO 2024 and solving 11 of 12 or all 12 Putnam 2025 problems.The cited systems include AlphaProof, Seed-Prover 1.5, AxiomProver, and Numina-Lean-Agent.
  • Beyond benchmarks, systems including Aristotle and AxiomProver have formalized open Erdős problems in Lean and other research conjectures, with some projects relying on substantial human guidance.

3 Overview of the Framework

The framework pairs Rethlas, which generates and verifies candidate informal proofs, with Archon, which formalizes them in Lean 4 and fills gaps. The agents use theorem retrieval, iterative reasoning, decomposition, memory, and formal verification to support scalable proof development.

  • Archon: Archon translates informal proofs into Lean 4, while its Plan Agent and Lean Agent divide decomposition, guidance, and formal proof execution.An informal agent can supply natural-language sub-proofs or alternative strategies when the Lean Agent encounters obstacles.
  • Rethlas: Rethlas generates candidate informal proofs and iteratively revises them using feedback from a separate verification agent.
  • Rethlas: Rethlas combines mathematical reasoning primitives—including examples, counterexamples, retrieval, decomposition, direct proving, recursive proving, and failure analysis—to explore solution strategies.
  • Rethlas: Matlas retrieves mathematically relevant statements through semantic vector search, using a structured corpus of approximately 13.6 million arXiv-based statements.The newer Matlas system is described separately as a curated corpus built from published papers and textbooks.
  • Rethlas: Rethlas stores intermediate artifacts such as examples, counterexamples, and subgoal plans in working memory for later reuse and coherence.
  • Archon: Formal verification reduces correctness checking to compilation and inspection of whether the formal statement and definitions preserve the intended mathematics.The framework adopts Lean 4 as its formal language and relies on Mathlib’s community-maintained library.
  • Archon: Scaling Archon to harder projects exposes repeated dead ends and difficulty locating expanding informal references, motivating enhancements for persistence and reference management.

4 Automated Resolution of Anderson’s Open Problem

The paper’s central case study targets Anderson’s open problem in commutative algebra and presents the generated proof alongside its formalization. The section also traces the problem’s mathematical background and discovery process.

  • Section 4 introduces the background and statement of Anderson’s open problem in commutative algebra.
  • The section presents Rethlas’s natural-language proof and traces the step-by-step discovery process that produced it.
  • Archon’s Lean 4 formalization of the proof is discussed as the final component of the case study.

2. R is weakly quasi-complete if the above condition holds for all decreasing sequences with T

Rethlas explored competing constructions for Anderson’s question and found a counterexample, which Archon then formalized and verified in Lean 4.

  • Anderson asked whether weak quasi-completeness implies quasi-completeness for Noetherian local rings.
  • After about 45 minutes, Rethlas established that a weakly quasi-complete ring need not be quasi-complete.
  • Rethlas’s search located Jensen’s difficult-to-find characterization of completions with trivial generic formal fiber.
  • The construction uses a ring whose completion has trivial generic formal fiber and whose quotient by a prime element is not analytically irreducible.
  • Rethlas abandoned unsuccessful plans, identified T = C[[x, y, z]]/(x2 −yz), and developed a clearer Jensen-based construction.
  • Archon translated the proof into Lean 4, filled implicit gaps, and verified the project with lake build and Comparator.
  • Human guidance reduced the remaining proof time from 3 hours and 43 minutes to 2 hours and 12 minutes in a controlled ablation.

5 Capabilities of the Informal and Formal Agents

Rethlas resolves and explores research-level problems, while Archon supports formal proof development; the algebraic-group case provides a detailed example of Rethlas’s capabilities.

  • 5 Capabilities of the Informal and Formal Agents: Rethlas’s case studies cover informal reasoning, mathematical discovery, algebraic groups, and p-adic Hodge theory.
  • 5.1.1 Rethlas for Automated Problem Solving in Algebraic Groups: For algebraic groups, Rethlas addressed a previously unrecorded rational conjugacy problem for one-parameter subgroups.
  • 5.1.1 Rethlas for Automated Problem Solving in Algebraic Groups: The easier split, reductive, and perfect-field cases were provable by both Rethlas and GPT-5.5 Pro.
  • 5.1.1 Rethlas for Automated Problem Solving in Algebraic Groups: Rethlas proved injectivity of X∗(G)/G(k) → X∗(GK)/G(K) after 44 minutes.
  • 5.1.1 Rethlas for Automated Problem Solving in Algebraic Groups: For the general case, Rethlas produced a correct solution, whereas GPT-5.5 Pro produced no meaningful solution.
  • 5.1.1 Rethlas for Automated Problem Solving in Algebraic Groups: The proof reduces first to quasi-reductive groups and then uses relative and absolute Weyl groups and root systems.
  • 5.1.1 Rethlas for Automated Problem Solving in Algebraic Groups: Rethlas’s proof depended on a restricted citation because the key copyrighted theorem was inaccessible, leaving the substitute survey statement incomplete.
  • 5.1.1 Rethlas for Automated Problem Solving in Algebraic Groups: Rethlas searched broadly, filtered unsuitable references, generated multiple plans, and organized the proof into five lemmas plus the main theorem.

2. Focused search

Rethlas’s focused search built technical understanding and generated two main proof routes for the algebraic-group problem.

  • Rethlas searched for solvable-group structure and found results used to support the algebraic-group reductions.
  • It located the Borel–Tits theorem in two identical references and chose to cite one of them.
  • A search for the relation between absolute and relative roots was constrained by failure to download a key copyrighted reference.
  • Toy-model analysis found injectivity in G = Ga ⋊Gm, prompting Rethlas to abandon counterexample searches and pursue a proof.
  • Rethlas generated two routes: a full pseudo-reductive quotient plan and a split-then-wound plan.
  • Plan A successively quotients by maximal split unipotent and central split torus subgroups, then studies pseudo-reductive groups through relative roots and Weyl groups.
  • Plan B quotients to the quasi-reductive case and proves it using relative roots and the relative Weyl group.

5. Attempts of Plan A and B

The paper follows Rethlas’s alternative proof plans from theorem-guided reductions through assembly, while Archon formalizes the resulting arguments and manages substantial proof gaps. Additional case studies show Rethlas strengthening conjectures and finding counterexamples, whereas Archon’s formalization remains constrained by efficiency and code-quality limitations.

  • Attempts of Plan A and B: Rethlas abandoned Plan A after identifying a potential torus-shear gap and instead completed Plan B using CGP relative root theory.The agent judged the reduction to G2 unnecessary and riskier, then used a toy example to identify the key ingredient.
  • Attempts of Plan A and B: Rethlas assembled the remaining details into a clearly stated Markdown proof whose logical steps were accepted by the natural-language verifier.The resulting output included the cited theorems and the argument connecting them.
  • Additional research-level problems: Rethlas strengthened a p-adic Hodge-theory theorem by replacing g ≫r with the explicit bound g ≥r2 + 1 and removing nilpotency.The strengthened result also partially explains why the original growth condition was needed.
  • Additional research-level problems: Rethlas found a genus-2, rank-36 counterexample with nonzero, non-nilpotent Higgs field when the condition g ≫r is removed.The example is a proper smooth rigid curve over C = Cp with a lift-independent Hitchin-small Higgs bundle.
  • Archon’s formalization capabilities: Archon can fill omitted arguments, refactor failed constructions, and replace unavailable formal infrastructure with alternative proof strategies.Reported examples include coefficient-level injectivity arguments, self-diagnosed failures involving Zorn’s lemma, and an independently found Kaplansky-criterion route.
  • Observed limitations: Archon’s recurring limitations include inefficient overthinking, dependence on targeted expert guidance, and verbose proofs that require human effort to align with Mathlib conventions.These tendencies do not necessarily prevent completion, but they reduce efficiency and hinder potential upstream contribution.

6 Conclusion

The framework combines theorem-guided informal proof discovery with Lean-based formalization to address research-level mathematics. It resolves an open commutative-algebra problem with essentially no human intervention and demonstrates broader research assistance, while retaining practical limits around guidance and formal-code quality.

  • Framework: The framework combines Rethlas for theorem-guided natural-language reasoning with Archon for Lean 4 formalization and autonomous gap filling.Matlas supports discovery of relevant results, while LeanSearch supports task decomposition and formal proof execution.
  • End-to-end result: The system solved an open commutative-algebra problem and automatically formalized its proof with essentially no human intervention.The paper attributes the informal success largely to Matlas’s discovery of relevant theorems from adjacent fields.
  • Additional capabilities: Rethlas proved an expert-level algebraic-groups problem, assisted active p-adic Hodge-theory research, strengthened conjectures, and constructed counterexamples.The algebraic-groups proof was contrasted with a completely incorrect proof produced by GPT-5.5 Pro in the reported comparison.
  • Human-AI collaboration: The framework reduces human labor by enabling natural interaction with formalization agents that can receive mathematical guidance, error reports, references, and elaborations.The paper presents this interaction as requiring only one or two mathematically trained people and almost no formalization expertise.
  • Conclusion: Informal and formal agents can cooperate on genuine open problems while limiting human involvement primarily to checking the semantic correctness of statements.The paper presents this cooperation as a concrete example of substantial automation in mathematical research.

A Mathematical Proof of Anderson’s Open Problem

The automated pipeline constructs a Noetherian local ring that is weakly quasi-complete but not quasi-complete, giving a negative answer to Anderson’s question. The proof uses completion, formal-fiber criteria, and a quotient that fails weak quasi-completeness.

  • Proof setup: The section presents the construction and proof of Anderson’s open problem as generated and formally verified by the complete automated pipeline.The human authors refactored the original AI-produced proof only for exposition and clarity, without changing its logical content.
  • Problem and definitions: Anderson asked whether weak quasi-completeness implies quasi-completeness for Noetherian local rings.The section answers this question negatively.
  • Construction strategy: The construction seeks a Noetherian local domain A with trivial generic formal fiber and a quotient A/aA that is not analytically irreducible.These conditions respectively ensure that A is weakly quasi-complete and that A/aA is not weakly quasi-complete.
  • Construction strategy: A complete 2-dimensional Cohen–Macaulay local domain T with a nonprincipal height-one prime Q supplies the structural input for Jensen’s construction.The ring also satisfies |T| = |T/M|, and its completion is used to obtain a 2-dimensional local UFD A.
  • Verification: Jensen’s construction yields a local UFD A with completion T and trivial generic formal fiber, so Farley’s criterion makes A weakly quasi-complete.The generic formal fiber is local with maximal ideal (0), hence every nonzero prime of the completion has nonzero contraction to A.
  • Verification: The quotient A/aA is a one-dimensional Noetherian local domain that is not analytically irreducible and therefore is not weakly quasi-complete.The argument derives this from the nonprincipal prime Q and the fact that T/aT is not a domain.
  • Conclusion: A is weakly quasi-complete while its homomorphic image A/aA is not, proving that A is not quasi-complete.This establishes a weakly quasi-complete Noetherian local ring that is not quasi-complete.

B Mathematical Proof of the Algebraic Group Problem

The paper proves that rational conjugacy of 1-parameter subgroups over an algebraic extension already descends to the base field. The proof reduces through split unipotent radicals, then uses torus conjugacy and relative root-system chambers in the k-wound case.

  • Theorem: For a smooth connected affine group G over k and an algebraic extension K/k, the natural map on rational conjugacy classes of 1-parameter subgroups is injective.Equivalently, k-cocharacters that become conjugate over K were already conjugate over k.
  • Theorem: The result remains valid for general field extensions K/k, according to the human-expert remark.The stated proofs did not use the assumption that K/k is algebraic.
  • Reduction: Vanishing of H1(k,U) for k-split smooth connected unipotent groups makes rational points lift through exact sequences.This permits quotienting by the split unipotent radical without losing control of conjugacy over k.
  • Reduction: After quotienting by the maximal k-split unipotent radical, the remaining unipotent radical is k-wound, reducing the general theorem to the wound case.The lifting argument transfers conjugacy from the quotient back to the original group.
  • Geometric lemma: Over an algebraically closed field, cocharacters in a maximal torus that are conjugate by the group are conjugate by the torus normalizer.The proof places both tori in a connected centralizer and applies maximal-torus conjugacy there.
  • Wound case: The relative root system and its Weyl group provide the chamber argument that completes the descent of conjugacy to k.The proof uses the identification of Weyl-group elements with representatives in the normalizer of the maximal split torus.
  • Wound case: In the k-wound case, every cocharacter has a unique representative in the closed dominant chamber under the k-rational normalizer.If two cocharacters become conjugate over an algebraic extension, their unique dominant representatives coincide, so they are already conjugate over k.

C Raw Output of Anderson’s Open Problem (Rethlas + GPT-5.4 xhigh)

Rethlas constructs a counterexample to Anderson’s open problem, while the argument reduces the result to properties of a specially chosen complete local ring and Jensen’s theorem. The resulting ring is weakly quasi-complete but not quasi-complete, and its quotient is not weakly quasi-complete.

  • Problem and construction: T is a complete 2-dimensional Cohen–Macaulay local domain, and its height-one prime Q=(x,y)T is nonprincipal.The quotient description establishes that T is a domain and Cohen–Macaulay; Q is shown to require at least two generators.
  • Problem and construction: The target is a 2-dimensional local UFD A with completion T and local generic formal fiber of maximal ideal (0).Here T = C[[x,y,z]]/(x^2-yz).
  • Jensen construction: Jensen’s corollary yields a local UFD A with completion T and generic formal fiber local with maximal ideal (0).The construction applies Jensen’s criterion with P=(0).
  • Quotient construction: The contraction q=Q∩A has height one and equals aA for a prime element a, so A/aA is a one-dimensional Noetherian local domain.The height calculation uses faithful flatness, and principality follows because A is a UFD.
  • Conclusion: Thus A is weakly quasi-complete but not quasi-complete, providing the required counterexample.A is weakly quasi-complete because every nonzero prime of its completion meets A; its bad quotient prevents quasi-completeness.
  • Quotient construction: A/aA is not analytically irreducible and therefore is not weakly quasi-complete.Its completion is T/aT, which is not a domain; the one-dimensional equivalence then gives the conclusion.

F Raw Output for the Algebraic Group Problem (GPT-5.5 Pro)

The algebraic-group case study concerns injectivity of cocharacter conjugacy after algebraic field extension. The supplied raw output claims a general proof, but the paper explicitly reports that this proof is incorrect because its reduction to the perfect-field case fails.

  • Attempted proof: The attempted proof reduces the comparison to the perfect closure kperf and uses conjugacy over an algebraic closure.It constructs a centralizer torsor and descends a point through a finite purely inseparable extension.
  • Claimed conclusion: The raw output concludes that cocharacters conjugate over K were already G(k)-conjugate.It presents this as equivalent to injectivity of the displayed map.
  • Caveat: The paper states that this proof is completely wrong because the naive reduction to the perfect-field case does not work.It also reports that a second GPT-5.5-Pro test, supplied with special cases, again produced an incorrect proof.

H Human-Provided Proof Blueprint

The blueprint formalizes a proof that Ssub is a UFD by reducing it to an intersection of localized polynomial rings, proving the intersection is Krull, and applying valuation-based factorization. It also records the transfinite-construction context and an alternative algebraic route used by Archon.

  • The blueprint targets proving that Ssub is a UFD.
  • Step 1: Reduction to ˜R: Because localization preserves the UFD property, it suffices to prove that ˜R is a UFD.
  • Steps 2–3: UFD and Krull structure: A1 and A2 are UFDs and Krull domains, and their finite intersection ˜R is also a Krull domain.
  • Step 4: Prime factors: Prime factors of y1 and y2 remain prime in ˜R because their valuation profiles have value 1 at exactly one DVR and 0 elsewhere.
  • Step 5: Localization: After inverting y1y2, ˜R becomes a localization of a polynomial UFD, enabling factorization arguments in the localized ring.
  • Step 6: Applying Nagata’s lemma: Valuation profiles pull factorizations back from ˜R[y−1] and show the resulting factors remain prime in ˜R.
  • Step 7: Conclusion: Since every element of ˜R factors into primes, ˜R and then its localization Ssub are UFDs.
  • Transfinite construction: Formalizing Jensen’s construction requires explicit transfinite recursion and bookkeeping beyond the high-level descriptions in the source papers.

I.1 Autonomous gap-filling in proof details

Archon autonomously fills omitted proof details by constructing explicit formal arguments, diagnosing mathematical errors, and adapting proof strategies to limitations in the available library infrastructure.

  • Autonomous gap-filling: Archon supplies non-trivial arguments omitted from informal proofs, including an injectivity proof for a power-series isomorphism.
  • Autonomous gap-filling: For the isomorphism, Archon constructs a coefficient-level quotient function and verifies term-by-term divisibility by x2 −yz.
  • Autonomous gap-filling: Archon correctly justifies |T| = |T/m| = |C| using the continuum identity c^ℵ0 = c.
  • Self-diagnosis of mathematical errors: An initial construction incorrectly replaced explicit transfinite recursion with Zorn’s lemma and identified cardinality below the continuum with countability.
  • Self-diagnosis of mathematical errors: Archon diagnosed that Zorn’s lemma lacked the intermediate-stage control required and that the countability assumption was unjustified without the Continuum Hypothesis.
  • Discovery of alternative proof strategies: Because Mathlib lacked Krull-domain infrastructure, Archon used Kaplansky’s criterion to establish the UFD result directly and concisely.

J Statement Verification via Comparator

Comparator verifies that Archon’s formal project proves the intended theorem exactly, passes the complete build, and uses only standard Lean axioms. A short specification lets human reviewers inspect semantic correctness independently of the proof code.

  • The full Lean project passes lake build, confirming that all proof obligations are discharged.
  • Comparator confirms that the theorem in the full project matches a short human-readable specification and uses only standard Lean axioms.
  • The specification file contains definitions of quasi-completeness and weak quasi-completeness together with the main theorem statement.
  • A human reviewer can check the semantic correctness of the specification’s 30 lines without knowing the proof or the rest of the codebase.
  • The main theorem asserts the existence of a weakly quasi-complete Noetherian local ring that is not quasi-complete.
  • Comparator verifies that main_theorem fills the intentional sorry with a complete proof matching the statement exactly.
Loading 2604.03789v2…