Automated Conjecture Resolution with Formal Verification

• LLMs have progressed from elementary mathematics to research-level reasoning, but FrontierMath Tier 4 pass@1 accuracy remains limited, reaching 38% for GPT-5.4-Pro (web).The passage reports 4% for o3-mini and 15% for GPT-5 before the 38% result for GPT-5.4-Pro (web).Source: §1 · p. 2
• Formal verification addresses the unreliable, labor-intensive evaluation of research-level mathematical reasoning by enabling rigorous checking in a precise symbolic language.Natural-language imprecision can cause errors even in expert assessment and peer review, whereas formalized arguments can be checked with complete rigor.Source: §1 · p. 2
• Rethlas explores candidate solution paths using theorem retrieval, while Archon converts informal proofs into verified Lean 4 projects through planning, iterative formalization, and persistent memory.Archon uses the formal theorem search engine LeanSearch [26] and is designed for correctness and scalability.Source: §1 · p. 2
• The framework demonstrates strong mathematical capability by filling non-trivial gaps left in the references and natural-language proof; its formalization also passes Comparator3’s check.Source: §1 · p. 3
• Separate evaluations show Rethlas proving an unrecorded expert-level algebraic-groups problem and supporting conjecture refinement, while Archon formalizes two research-level problems with zero or minimal hints.Rethlas also identifies an unnecessary assumption, sharpens a condition, and constructs a counterexample; Archon succeeds autonomously on one formalization and with a one-sentence hint on the other.Source: §1 · p. 3

2.1 Agents for Natural Language Reasoning

• Verification-and-refinement agents substantially improve mathematical problem solving, with [32] solving 5 of 6 IMO 2025 problems and Aletheia [24] autonomously tackling four Erdős problems while addressing additional research tasks.Aletheia also solved 6 of 10 FirstProof problems [22], while FullProof [10] combines AI handling of special cases with human insights for general solutions.Source: §2.1 · p. 3

2.2 Agents for Formal Reasoning

• Lean 4 agents achieve strong competition-level results, including silver-medal performance by AlphaProof, 11 of 12 Putnam problems by Seed-Prover 1.5 [13], and all 12 by AxiomProver [8] and Numina-Lean-Agent [42].Aristotle [4] combines proof search, MCTS, and informal reasoning to achieve IMO 2025 gold-medal performance and provide a public API.Source: §2.2 · p. 3
• Formal reasoning systems also reach research-level mathematics, formalizing open Erdős problems, Fel’s conjecture [12], the Brascamp–Lieb theorem [42], and a mathematical-physics result [34].These efforts range from autonomous formalization to collaboration involving one or more human experts.Source: §2.2 · pp. 3–4
• Gauss scales formal verification to approximately 200,000 lines of Lean code for Fields Medal–winning sphere-packing proofs, using a human blueprint for dimension 8 and autoformalization for dimension 24.Leanstral additionally provides an open-source agent for research-level proof engineering.Source: §2.2 · p. 4

3 Overview of the Framework

• Rethlas generates candidate informal proofs, while Archon translates them into Lean 4 and fills formalization gaps until the resulting project compiles.The two agents form the framework’s informal-reasoning and formal-verification components.Source: §3 · p. 4

3.1 Rethlas: The Informal Agent

• Rethlas iteratively alternates generation and verification, using examples, counterexamples, theorem retrieval, decomposition, direct or recursive proving, and failure analysis to revise candidate proofs.Its skills are selected adaptively rather than applied in a fixed order, with Matlas providing semantic search over approximately 13.6 million arXiv mathematical statements.Source: §3.1 · pp. 4–5

3.2 Archon: The Formal Agent

• Archon formalizes an informal proof as a Lean 4 project grounded in Mathlib, collecting dependencies, organizing definitions and lemmas, consulting other agents or sources, and refining strategies until compilation succeeds.Formal verification makes correctness depend on the compiled statement and supporting definitions faithfully capturing the intended mathematics.Source: §3.2 · p. 6

3.2.1 System Architecture and Workflow Design

• Archon uses a Plan Agent and constrained Lean Agent across scaffolding, iterative proving, and verification-and-polish phases, supported by informal-agent consultation and LeanSearch retrieval.The dual-agent design reduces context pollution and task aversion, while LeanSearch helps determine whether needed results already exist in Mathlib.Source: §3.2.1 · p. 7

3.2.2 Enhancements for Conjecture Formalization

• For larger formalization projects, Archon adds session summaries, global status tracking, a Review Agent, structured prompts, and separated reference management to prevent repeated dead ends and improve strategy control.These enhancements keep task-relevant context clean and let the Plan Agent detect stalls across sessions, supporting the full-scale formalization.Source: §3.2.2 · p. 8

4 Automated Resolution of Anderson’s Open Problem

• The section covers Anderson’s problem, Rethlas’s proof overview and discovery process, and Archon’s formalization in Lean 4.Source: §4 · p. 8

4.1 Anderson’s open problem

• The problem is formulated for a Noetherian local ring (R, m).Source: §4.1 · p. 8
• R is defined as quasi-complete when every decreasing sequence of ideals {A_n}_n≥1 and every integer k≥1 admit an associated s_k.Source: §4.1 · p. 8

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

• Theorem 1 gives a negative answer to Anderson’s question by exhibiting a weakly quasi-complete ring that is not quasi-complete.The question asks whether weak quasi-completeness implies quasi-completeness for Noetherian local rings.Source: §2 · p. 9

4.2 Overview of the mathematical proof

• The proof constructs a ring A whose completion T has trivial generic formal fiber and whose quotient A/aA is one-dimensional, Noetherian, and not analytically irreducible.Jensen’s characterization [35, Corollary 2.4] enables the construction; a nonprincipal height-one prime yields the required quotient obstruction.Source: §4.2 · p. 9

4.3 Rethlas’ discovery process

• Rethlas progressed from broad and focused literature searches through three failed or incomplete plans to Plan D, based on Jensen’s result and T = C[[x, y, z]]/(x2 −yz).The final plan constructs a weakly quasi-complete local UFD whose completion is nonfactorial and contains a nonprincipal height-one prime.Source: §4.3 · pp. 9–10

4.4 Archon’s formalization process

• 19,448 lines of Lean 4 code across 42 files were completed in approximately 80 hours, and the entire project passed lake build without errors.Comparator6 additionally confirmed agreement with a human-reviewed specification and use of only standard Lean axioms.Source: Figure 6 · p. 11, §4.4 · p. 11
• Archon autonomously filled omitted proof gaps, diagnosed failed strategies, refactored across sessions, and bypassed missing Mathlib definitions with alternative arguments.The formalization covered the main theorem, supporting lemmas, and results from six external papers, including Jensen.Source: §4.4 · pp. 10–11
• Human guidance resolved the remaining obligations in 2 hours 12 minutes versus 3 hours 43 minutes autonomously, roughly 70% longer without intervention.The guidance supplied reusable intermediate results rather than redirecting Archon from its existing Kaplansky-criterion strategy.Source: §4.4 · p. 11

5 Capabilities of the Informal and Formal Agents

• The section also tests Archon on formalizing proofs for two research-level problems from FirstProof [2].The broader section therefore covers both Rethlas’s informal reasoning and discovery and Archon’s formal proof translation.Source: §5 · p. 12

5.1 Rethlas for Informal Mathematical Reasoning and Discovery

• Beyond this case, Rethlas supported mathematical discovery by proving a conjecture, identifying essential hypotheses, sharpening a condition into an explicit bound, and constructing counterexamples when a key condition was removed.These capabilities were demonstrated in an example from p-adic Hodge theory, alongside other documented open-problem applications including, [19], and [37].Source: §5.1 · p. 12

5.1.1 Rethlas for Automated Problem Solving in Algebraic Groups

• Rethlas produced a correct solution to a previously unrecorded algebraic-group problem, whereas GPT-5.5 Pro produced a completely wrong proof.The correct solution used GPT-5.5 xhigh for generation and GPT-5.4 xhigh for verification, apart from a citation-substitution issue.Source: §5.1.1 · p. 12
• After 44 minutes, Rethlas proved that X∗(G)/G(k) → X∗(G_K)/G(K) is injective, affirmatively resolving the rational conjugacy problem.The result concerns connected smooth affine group schemes and arbitrary field extensions as stated in the problem.Source: §5.1.1 · pp. 12–13
• The solution’s main limitation was citation substitution: lacking access to [18, Theorem C.2.15], Rethlas cited [17, Theorem 5.3.2(iv)], whose statement omits the required assertion.The survey proof refers back to [18, Theorem C.2.15], but the survey theorem itself is insufficient as stated.Source: §5.1.1 · p. 13
• Rethlas’s proof used five lemmas and first reduced the problem to quasi-reductive groups before handling the technically difficult quasi-reductive case.The reduction uses the maximal-split smooth connected unipotent normal subgroup, triviality of H1(k, U), and conjugacy of maximal split k-tori.Source: §5.1.1 · p. 13
• In the quasi-reductive case, Rethlas related rational conjugacy classes to relative and absolute Weyl-group quotients through the relationship between relative and absolute root systems.The key structural descriptions use X∗(S)/W(G, S) and X∗(T_ks)/W(G_ks, T_ks), with the restriction map between root systems supplying the connection.Source: §5.1.1 · p. 13
• Rethlas’s discovery process combined broad theorem search with filtering and located technical resources including [44, Theorem 3.1.3],,, [30], and.The search also used Brian Conrad’s MathOverflow answer and explored cohomological obstructions or pathological unipotent behavior as possible routes to counterexamples.Source: §5.1.1 · p. 14, Figure 7 · p. 14

Focused theorem search

• Rethlas searched the structure of solvable groups and found [16, Corollary 3.12, Corollary 4.4, Theorem 5.4, Corollary 5.12].Source: §2 · p. 14
• It retrieved two identical versions of the Borel–Tits theorem, chose to cite [17, Theorem 4.2.9], and failed to download while seeking the absolute–relative root relation.Source: §2 · p. 14

3. Counterexample hunt and toy examples

• After finding no counterexample through literature and cocharacter searches, Rethlas analyzed G = Ga ⋊Gm with positive weight n, where injectivity holds, and switched to proving injectivity.Source: §2 · p. 14

4. Plan generation

• Plan A reduces G by quotienting the maximal k-split smooth connected unipotent normal subgroup, then the maximal central k-split torus, before reaching a pseudo-reductive group.Source: §2 · p. 14
• Plan A proves the pseudo-reductive case using relative roots and the relative Weyl group, while Plan B instead reduces to the quasi-reductive, or wound unipotent, case.Source: §2 · pp. 14–15
• Plan B proves the quasi-reductive case using relative roots and the relative Weyl group, with three lemmas and the main theorem.Source: §2 · p. 15

5. Attempts of Plan A and B

• Rethlas abandoned Plan A because its split-torus quotient reduction risked a torus-shear gap, while Plan B used relative root theory to finish all technical subgoals.It then assembled the remaining details into a Markdown proof accepted by the natural-language verifier.Source: §5 · p. 15

5.1.2 Rethlas for Mathematical Discovery in p-adic Hodge Theory

• Rethlas strengthened the p-adic Hodge conjecture by removing nilpotency and replacing g ≫r with the explicit bound g ≥r2 + 1, proving θ = 0 under those conditions.The theorem assumes g ≥2, semistability, and cohomological lift-independence.Source: §5.1.2 · p. 16
• Rethlas also found counterexamples after dropping the genus condition: for sufficiently large p, genus g = 2 admits a rank r = 36 lift-independent bundle with nonzero, non-nilpotent θ.The counterexample was derived from Landesman–Litt’s solution to Prill’s problem.Source: §5.1.2 · p. 16

5.2.1 Additional formalization results

• Archon formalized FirstProof Problems 4 and 6, completing Problem 6 autonomously and requiring one natural-language hint for Problem 4.The runs took approximately 50 and 30 hours, respectively, with costs of approximately $1,200 and $750.Source: §5.2.1 · pp. 16–17

5.2.2 Notable mathematical capabilities

• Archon autonomously filled implicit proof gaps, including coefficient-level injectivity arguments and a well-founded recursive construction preserving invariants through successor and limit stages.These capabilities extended from missing sub-arguments to constructions described only schematically in source papers.Source: §5.2.2 · p. 17
• Archon diagnosed failed approaches and discovered alternative routes, replacing an invalid Zorn-and-countability strategy with recursion and cardinal arithmetic and replacing unavailable infrastructure with Kaplansky’s criterion or Euler–Jacobi.The Euler–Jacobi route discharged a residue-theorem obligation algebraically, while Kaplansky’s criterion replaced unavailable Krull domain theory.Source: §5.2.2 · p. 17

5.2.3 Observed limitations

• Archon’s recurring limitations were inefficient overthinking during difficult obligations and verbose, non-idiomatic Lean code requiring substantial human effort for Mathlib alignment.Targeted prompt guidance improved throughput, but case-by-case expert judgment remained preferable to rigidly enforcing the reference proof.Source: §5.2.3 · pp. 17–18

6 Conclusion

• The two-agent framework solved an open problem in commutative algebra and automatically formalized its proof with essentially no human intervention.Rethlas uses Matlas for theorem discovery, while Archon uses LeanSearch for task decomposition, guidance, and formalization.Source: §6 · p. 18
• Rethlas handled additional research-level problems by proving an expert-level algebraic-groups problem, refining p-adic Hodge conjectures, and constructing counterexamples when conditions were removed.It strengthened statements, exposed redundant hypotheses, and helped refine correct formulations rather than merely proving fixed claims.Source: §6 · p. 18
• Archon formalized natural-language proofs of two research-level problems, completing one autonomously and the other with only a one-sentence hint.These case studies support the generality of the capabilities observed in the Anderson case.Source: §6 · p. 18
• Matlas enabled Rethlas to retrieve and apply highly technical methods from adjacent fields, supporting cross-domain reasoning comparable to expert-level interdisciplinary discussions.In Anderson’s open problem, Rethlas identified and applied methods connected to Jensen’s paper.Source: §6 · p. 18
• The framework is presented as broadly generalizable, reduces formalization labor to one or two mathematically trained people, and supports natural interaction without exhaustive formal detail.Users can highlight difficulties, identify errors, suggest references, and elaborate on challenging points.Source: §6 · p. 19
• Informal and formal agents cooperate by generating plausible proofs, formalizing them, and filling missing details, while humans primarily verify semantic correctness.The conclusion characterizes this cooperation as a concrete example of substantially automating mathematical research.Source: §6 · p. 19

A Mathematical Proof of Anderson’s Open Problem

• The complete automated pipeline generated and formally verified the mathematical proof, while human authors only refactored it for exposition; related commutative-algebra solutions appear in [37].The formal verification is presented as part of the paper’s automated resolution of Anderson’s open problem.Source: A Mathematical Proof of Anderson’s… · p. 23

Reduction of the problem

• The proof reduces the problem to constructing a Noetherian local domain A with trivial generic formal fiber and a prime element a whose quotient A/aA is not analytically irreducible.Farley’s and Anderson’s criteria convert these conditions into weak quasi-completeness of A and failure of weak quasi-completeness for A/aA.Source: Reduction of the problem · pp. 23–24

Construction of the complete local domain T

• The construction begins with a complete 2-dimensional Cohen–Macaulay local domain T whose height-one prime Q=(x,y)T is not principal and whose cardinality equals that of its residue field.These properties respectively support Jensen’s construction and the later verification of the quotient condition.Source: Construction of the complete local… · p. 24

Construction of the local UFD A

• Jensen’s result applied to T produces a 2-dimensional local UFD A with completion isomorphic to T and generic formal fiber local with maximal ideal (0).The required hypotheses follow from T’s completeness, cardinality, depth, domain structure, and Cohen–Macaulay property.Source: Construction of the local UFD A · pp. 24–25

Verification that A is the desired counterexample

• The generic formal fiber of A is trivial, so Farley’s criterion establishes that A is weakly quasi-complete.Every nonzero prime of the completion has nonzero contraction to A.Source: Verification that A is the desired… · p. 25
• Using the nonprincipal prime Q, the proof finds a prime element a∈A such that A/aA is a one-dimensional Noetherian local domain that is not analytically irreducible or weakly quasi-complete.The key step is that aT is not prime, making the completed quotient—and hence A/aA—not a domain.Source: Verification that A is the desired… · p. 25

Conclusion

• Theorem 9 constructs a weakly quasi-complete Noetherian local ring that is not quasi-complete, providing a negative answer to Anderson’s question.The AI-generated proof was human-refactored only for exposition and clarity, without changing its logical content.Source: Definitions and statement of the main… · p. 23, A Mathematical Proof of Anderson’s… · p. 23, Conclusion · p. 25

B Mathematical Proof of the Algebraic Group Problem

• The complete automated pipeline produces and verifies the proof of Theorem 15, with human refactoring limited to exposition and clarity.The theorem states that if two k-cocharacters become conjugate over an algebraic extension K/k, they were already conjugate over k.Source: B Mathematical Proof of the Algebraic… · p. 26, Definitions and statement of the theorem · p. 26, Proof of the main theorem · p. 32

Split unipotent groups and rational points

• For k-split smooth connected unipotent groups, H1(k,U) vanishes, making rational points lift through exact sequences and preserving control of conjugacy over k.The proof uses a composition series with successive quotients isomorphic to Ga and H1(k, Ga) = 0.Source: Split unipotent groups and rational… · pp. 26–27

Reduction modulo the split unipotent radical

• Injectivity descends modulo the maximal k-split unipotent radical and lifts back using rational-point surjectivity and conjugacy of maximal split tori.The quotient has k-wound unipotent radical, while a pullback argument and uniqueness of sections complete the lifting step.Source: Reduction modulo the split unipotent… · pp. 27–28

A geometric normalizer lemma

• Over an algebraically closed field, cocharacters inside a fixed maximal torus that are conjugate by the group are conjugate by the torus normalizer.The argument centralizes one cocharacter and applies conjugacy of maximal tori in the resulting centralizer.Source: A geometric normalizer lemma · pp. 28–29

The wound case and relative dominant representatives

• In the k-wound case, every cocharacter has a unique representative in a closed relative dominant chamber, and extension-field conjugacy forces these representatives to coincide.Relative root systems and Weyl-group representatives in NH(S)(k) yield conjugacy over k.Source: The wound case and relative dominant… · pp. 29–31
• For groups with k-wound unipotent radical, the dominant-representative result proves injectivity of cocharacter conjugacy over every algebraic extension.After separately conjugating into a maximal split torus, Lemma 20 gives NH(S)(k)-conjugacy.Source: The wound case and relative dominant… · p. 31

Proof of the main theorem

• For an arbitrary smooth connected affine k-group, quotienting by its maximal k-split unipotent radical produces the wound case, and Lemmas 24 and 17 establish Theorem 15.The final conclusion is that conjugacy over K by G(K) implies conjugacy over k by G(k).Source: Proof of the main theorem · pp. 31–32

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

• Rethlas first chooses T=C[[x,y,z]]/(x^2-yz), proving it is a complete two-dimensional Cohen–Macaulay local domain with |T|=|T/M| and nonprincipal height-one prime Q=(x,y)T.The domain identification is T≅C[[u^2,uv,v^2]], while Q/MQ requires at least two generators.Source: C Raw Output of Anderson’s Open… · pp. 32–33
• Applying Jensen’s Corollary 2.4, Rethlas obtains a local UFD A with completion T and generic formal fiber local with maximal ideal (0).The application checks completeness, cardinality, depth two, associated-prime, nonmaximality, prime-subring, and Cohen–Macaulay conditions.Source: C Raw Output of Anderson’s Open… · p. 33
• Rethlas constructs a weakly quasi-complete Noetherian local ring A that is not quasi-complete, with a prime element a such that A/aA is not weakly quasi-complete.The construction uses a complete two-dimensional Cohen–Macaulay domain T, Jensen’s result to obtain A, and a non-analytically-irreducible quotient.Source: C Raw Output of Anderson’s Open… · pp. 34–35

D Output for the Anderson’s Open Problem (GPT-5.4 Pro)

• GPT-5.4 Pro presents a concrete alternative construction from Nagata’s appendix, taking a regular local ring A whose completion is k[[X,Y]], and states that A is weakly quasi-complete but not quasi-complete.The supplied passage gives the construction and claimed properties but does not provide the full intervening derivation.Source: D Output for the Anderson’s Open… · p. 36

A useful criterion

• The useful criterion characterizes weak quasi-completeness by completion-prime contractions: R is weakly quasi-complete iff every nonzero prime of its completion contracts nontrivially to R.The two directions are given as Lemmas 26 and 27.Source: A useful criterion · pp. 36–37

Step 1: A is weakly quasi-complete

• In the explicit construction, every nonzero prime of bA contracts nontrivially, while a quotient B=A/aA has a nonzero completion prime contracting to zero; hence A is weakly quasi-complete and B is not.The quotient argument uses characteristic p, coefficient-field exhaustion, Weierstrass division, and the resulting contraction computation.Source: Step 1: A is weakly quasi-complete · p. 37, Step 2: a quotient of A is not weakly… · p. 39

Conclusion

• The ring A = k_p[[X, Y]][k] is weakly quasi-complete, while B = A/aA is not, so A is not quasi-complete by the homomorphic-image criterion.This establishes a weakly quasi-complete ring that is not quasi-complete.Source: Conclusion · p. 39
• Rethlas’s counterexample is presented as new and non-constructive, whereas GPT-5.4-Pro found an explicitly constructed example that was previously given by Nagata for another purpose [48, Appendix A1, E3.1].Both approaches reduce to a weakly quasi-complete ring with a quotient that is not, using Farley’s result for the weakly quasi-complete condition.Source: Conclusion · pp. 39–40

E Raw Output for the Algebraic Group Problem (Rethlas + GPT-5.5 xhigh)

• If the k-unipotent radical is k-wound, every cocharacter is N_H(S)(k)-conjugate to a unique dominant representative, and extension-conjugate cocharacters share that representative.The proof uses relative and absolute root systems, Weyl-group orbits, and uniqueness in the closed dominant chamber.Source: E Raw Output for the Algebraic Group… · pp. 43, 45
• The general injectivity proof removes the maximal k-split unipotent radical, applies the k-wound case to the quotient, and lifts injectivity using H^1(k,U)=1.The lifting step relies on surjectivity from G(k) to the quotient’s k-points for k-split smooth connected unipotent kernels.Source: E Raw Output for the Algebraic Group… · pp. 40, 46
• For every smooth connected affine group G over k and algebraic extension K/k, the map X_*(G)/G(k) → X_*(G_K)/G(K) is injective.Thus k-homomorphisms G_m → G that become G(K)-conjugate were already G(k)-conjugate.Source: E Raw Output for the Algebraic Group… · pp. 45–46

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

• The GPT-5.5-Pro proof is completely wrong: its naive reduction to the perfect-field case and claimed bijectivity fail, including when tested through the webpage interface.The raw output nevertheless concludes that λ and µ are G(k)-conjugate, but the appendix explicitly rejects this conclusion.Source: F Raw Output for the Algebraic Group… · p. 47

G Correspondence between Natural Language Proof and Formalization

• The correspondence appendix links the informal proof’s main components to Lean 4 declarations and project files, including the main theorem and construction of T.It first describes correspondence for the main proof components, then explains how external results are formalized and where reference materials reside.Source: G Correspondence between Natural… · p. 48, Main theorem and definitions · p. 48

Main theorem and definitions

• The formalized construction defines T = C[[x, y, z]]/(x2 −yz) and verifies that it is a domain, complete local ring, Noetherian, M-adically complete, and Cohen–Macaulay of dimension 2.It also formalizes the prime height-one ideal Q and proves that Q is not principal.Source: Main theorem and definitions · p. 48

Verification (conditions (A) and (B))

• The formalization constructs A and verifies condition (A), including weak quasi-completeness, height-one contraction, principal height-one primes, and one-dimensional quotients.It also establishes condition (B) by proving the existence of a prime quotient that is not analytically irreducible.Source: Main theorem and definitions · p. 48, Verification (conditions (A) and (B)) · p. 48

Cited results from the literature

• Anderson’s results are formalized for one-dimensional WQC rings, proper quotients, and completeness implying quasi-completeness, with the latter following Anderson’s proof of Chevalley’s result.The completeness result appears in the background and is not directly required in the main proof chain.Source: Cited results from the literature · p. 49
• Farley’s characterization is formalized as the key tool for establishing condition (A), relating weak quasi-completeness to primes of the completion meeting the ring nontrivially.The formalization records this result in QuasiCompleteRing/QuasiCompleteRing.lean.Source: Cited results from the literature · p. 49
• Jensen’s prescribed-completion construction, building on Heitmann and Loepp, is formalized as a transfinite recursive procedure spanning approximately 15,000 lines of the Jensen directory.Its components cover recursion, close-up, Krull-domain verification, limit unions, adjoining transcendental elements, N-subrings, and application to T.Source: Cited results from the literature · p. 49

H Human-Provided Proof Blueprint; Mathematical setting

• The human blueprint targets S_sub as a UFD for a complete Noetherian local domain T, an N-subring R, coprime y1,y2, and transcendental x1,x2 satisfying c = x1y1 + x2y2.This alternative route uses a Krull-domain approach rather than the Kaplansky-criterion route pursued by Archon, and was supplied only for an ablation experiment.Source: H Human-Provided Proof Blueprint · pp. 49–50, Mathematical setting · p. 50

Formalization suggestions

• The blueprint formalization introduces Krull rings and valuation subrings generated by prime elements, then constructs the corresponding localization as a valuation subring.It relies on the fact that finite intersections of Krull rings with a common fraction field remain Krull and that localization at a prime element yields the needed valuation structure.Source: Formalization suggestions · p. 50

Proof

• The proof reduces to ˜R, shows the auxiliary rings are UFDs and Krull domains, proves ˜R is Krull with y1y2 represented by prime elements, and shows its localization is a UFD.The relation c = x1y1 + x2y2 identifies the doubly localized polynomial presentations, making the resulting ring a localization of the polynomial UFD R[x1].Source: Proof · pp. 50–51
• Archon concludes that S_sub is a UFD by proving a localized intermediate ring is Krull, establishing prime-factor behavior, and applying Nagata’s lemma.The argument factors elements after localization, proves pulled-back factors remain prime via valuation profiles, and uses preservation of the UFD property under localization.Source: Proof · p. 51

Supporting lemma: localization at a prime element in a Krull domain

• The supporting lemma proves that localizing a Krull domain A at the prime ideal generated by a prime element t produces a DVR.The proof uses discrete valuations to show the intersection of all powers of the maximal ideal is zero, completing the DVR criterion.Source: Supporting lemma: localization at a… · p. 51

I Detailed Mathematical Examples from the Formalization; I.2 Handling underspecified transfinite constructions

• Formalizing Jensen’s underspecified transfinite construction required explicit well-founded recursion, bundled stage data, cardinality bounds max(ℵ0, |{γ ≤α}|), and modular preservation proofs.Archon decomposed successor and limit stages into independently verifiable algebraic components, including preservation of UFD properties, prime extensions, and cardinality constraints.Source: I Detailed Mathematical Examples from… · p. 52, §I.2 · p. 52

I.4 Cross-session architectural refactoring

• Archon replaced an incorrect Zorn-based strategy with explicit well-founded recursion and generalized cardinal arithmetic, refactoring interdependent files across multiple sessions.The refactoring required maintaining the proof architecture across context boundaries and removing countability assumptions from the cardinality arguments.Source: §I.4 · p. 53

I.6 A single hint redirecting a stalled obligation; I.7 Bypassing missing infrastructure

• A human’s single suggestion to use Vieta’s formulas redirected a stalled root-location obligation, which Archon then completed algebraically within an hour, while it autonomously bypassed missing residue-theorem infrastructure using the Euler–Jacobi formula.All other obligations in Problems 4 and 6 required no human intervention, and the Euler–Jacobi alternative was not present in consulted reference material.Source: §I.6 · p. 53, §I.7 · pp. 53–54

I.1 Autonomous gap-filling in proof details

• Archon autonomously completed omitted nontrivial arguments, including an injectivity proof by constructing a coefficient-level quotient and proving kernel divisibility by x^2 − yz.This completed the isomorphism argument without consulting external references.Source: §I.1 · p. 52
• Archon also closed a cardinality gap by recognizing that the identity |T| = |T/m| = |C| depends on c^ℵ0 = c and applying the corresponding Mathlib lemma.The general equality κ^ℵ0 = κ need not hold for every infinite cardinal κ.Source: §I.1 · p. 52

I.3 Self-diagnosis of mathematical errors

• In its initial transfinite construction, Archon used Zorn’s lemma and equated cardinality below the continuum with countability, causing invalid cardinality bounds and failed limit-stage closure.The countability identification is valid under the Continuum Hypothesis but not provable in ZFC alone.Source: §I.3 · p. 52
• Archon diagnosed these failures without human guidance, identifying Zorn’s lack of intermediate-stage control and the unjustified countability assumption, then reformulating the construction correctly.The source papers did not explicitly warn against these pitfalls.Source: §I.3 · pp. 52–53

I.5 Discovery of alternative proof strategies

• For the UFD lemma corresponding to Lemma 4 of Heitmann, Archon avoided unavailable Krull-domain infrastructure that the original proof would have required.Mathlib lacked a formalized definition of Krull domains and related divisorial-ideal theory.Source: §I.5 · p. 53
• Archon instead applied Kaplansky’s criterion to prove the UFD result directly, producing a shorter formalization absent from the supplied reference papers.The alternative demonstrates adaptation to available library support rather than rigidly following the informal proof.Source: §I.5 · p. 53

• The entire project passes lake build, and Comparator confirms that the full theorem matches the short specification and uses only standard Lean axioms.These checks establish both discharged proof obligations and correspondence with the intended statement.Source: J Statement Verification via Comparator · p. 54
• The 30-line Challenge.lean specification defines quasi-completeness, weak quasi-completeness, and the main theorem statement for independent human review.It contains no proof details or other codebase components, allowing semantic inspection without knowledge of the formal proof.Source: J Statement Verification via Comparator · p. 54
• Comparator verifies that the full project discharges the intentional sorry and proves exactly the specification’s main_theorem declaration.The theorem asserts the existence of a weakly quasi-complete Noetherian local ring that is not quasi-complete.Source: J Statement Verification via Comparator · p. 54