arxiv: 2604.03789 · v1 · submitted 2026-04-04 · 💻 cs.LG · cs.AI

Recognition: no theorem link

Automated Conjecture Resolution with Formal Verification

Haocheng Ju , Guoxiong Gao , Jiedong Jiang , Bin Wu , Zeming Sun , Leheng Chen , Yutong Wang , Yuefeng Wang

show 7 more authors

Zichen Wang Wanyi He Peihao Wu Liang Xiao Ruochuan Liu Bryan Dai Bin Dong

Authors on Pith no claims yet

Pith reviewed 2026-05-13 18:01 UTC · model grok-4.3

classification 💻 cs.LG cs.AI

keywords automated mathematical reasoninglarge language modelsformal verificationLean 4commutative algebratheorem provingAI-assisted research

0 comments

The pith

An automated two-agent system resolves an open commutative algebra problem and produces a machine-verified Lean 4 proof with minimal human input.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a framework that pairs an informal reasoning agent with a formal verification agent to handle research-level mathematics. The informal agent explores solution strategies using theorem search tools and natural language primitives. The formal agent then translates those strategies into Lean 4 code, fills gaps through iterative refinement, and confirms correctness. The authors apply the system to an open problem in commutative algebra and obtain a fully verified proof with essentially no human intervention. This demonstrates that combining informal exploration with automated formal translation can reduce the effort required to settle and certify mathematical claims.

Core claim

The framework consists of Rethlas, which mimics human mathematicians by combining reasoning primitives with the Matlas theorem search engine to generate candidate proofs, and Archon, which uses LeanSearch to translate informal arguments into structured Lean 4 projects, iteratively refine them, and synthesize machine-checkable proofs. Applied to an open problem in commutative algebra, the system produces a correct formal proof in Lean 4 with essentially no human involvement.

What carries the argument

Two-agent pipeline in which the informal agent (Rethlas with Matlas) generates natural-language solution strategies and the formal agent (Archon with LeanSearch) decomposes, translates, refines, and verifies them into Lean 4.

If this is right

Strong theorem retrieval tools enable the discovery and application of cross-domain mathematical techniques.
The formal agent is capable of autonomously filling nontrivial gaps in informal arguments.
Informal and formal reasoning systems equipped with theorem retrieval tools can operate in tandem to produce verifiable results.
Human effort in mathematical research is substantially reduced.
The approach offers a concrete instantiation of human-AI collaborative mathematical research.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same two-agent structure could be tested on open problems in other areas such as algebraic geometry where partial informal arguments already exist.
Improving the informal agent's theorem retrieval precision might reduce the number of refinement cycles needed in the formal stage.
If the informal agent is replaced by a stronger model, the framework might handle problems that currently require more human scaffolding.
The pipeline suggests a route toward automated verification of larger bodies of conjectural mathematics once initial informal sketches are supplied.

Load-bearing premise

The informal reasoning produced by the first agent will be sufficiently complete and accurate that the formal agent can translate and complete it into a correct Lean 4 proof without substantial additional human guidance or correction.

What would settle it

Running the framework on the same commutative algebra problem and finding that Archon requires extensive human-written lemmas or corrections to produce a valid Lean 4 proof would falsify the claim of end-to-end automation with minimal intervention.

read the original abstract

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 for tackling research-level mathematical problems that integrates natural language reasoning with formal verification, enabling end-to-end problem solving with minimal human intervention. Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon. Rethlas mimics the workflow of human mathematicians by combining reasoning primitives with our theorem search engine, Matlas, to explore solution strategies and construct candidate proofs. Archon, equipped with our formal theorem search engine LeanSearch, translates informal arguments into formalized Lean 4 projects through structured task decomposition, iterative refinement, and automated proof synthesis, ensuring machine-checkable correctness. Using this framework, we automatically resolve an open problem in commutative algebra and formally verify the resulting proof in Lean 4 with essentially no human involvement. Our experiments demonstrate that strong theorem retrieval tools enable the discovery and application of cross-domain mathematical techniques, while the formal agent is capable of autonomously filling 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, substantially reduce human effort, and offer a concrete instantiation of human-AI collaborative mathematical research.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper describes a two-agent LLM setup that claims to have solved an open commutative algebra problem end-to-end and verified it in Lean 4, but supplies almost no concrete details on the conjecture, the proof, or the automation steps.

read the letter

The core contribution is an architecture that pairs an informal reasoning agent (Rethlas) using a custom theorem search tool (Matlas) with a formal agent (Archon) that decomposes the argument, refines it iteratively, and synthesizes Lean 4 proofs via another search engine (LeanSearch). They report using this to resolve a previously open problem in commutative algebra with essentially no human intervention after the initial setup. The retrieval components are presented as the practical enabler for pulling in relevant lemmas across domains, and the formal side is shown handling some nontrivial gaps through structured decomposition rather than pure prompting. That combination is a reasonable incremental step beyond earlier LLM math work that stayed informal or required heavy human scaffolding. The description of the workflow is clear enough that someone building similar tools could replicate the high-level flow. The main weakness is evidentiary. The abstract asserts success on an open problem and machine-checkable output, yet neither the conjecture statement, the informal sketch, the specific gaps encountered, the number of refinement rounds, nor any success-rate numbers appear in the provided material. Without those artifacts or logs it is difficult to judge whether the informal output was already close to formalizable or whether hidden edits occurred. The claim of autonomous gap-filling therefore rests on assertion rather than displayed evidence. This work is aimed at researchers combining LLMs with interactive theorem provers. A reader already experimenting with Lean agents or retrieval-augmented math systems could extract useful implementation ideas, but the paper would need the missing proof details and metrics before it could be cited with confidence. It is worth sending to peer review because the architecture is timely and the formal-verification angle is worth checking, even if the current version requires substantial revision to make the central result evaluable.

Referee Report

2 major / 2 minor

Summary. The paper introduces a hybrid framework with two LLM-based agents: Rethlas, which performs informal mathematical reasoning by combining primitives with the Matlas theorem search engine, and Archon, which translates informal arguments into Lean 4 proofs via structured decomposition, iterative refinement, and the LeanSearch formal theorem retrieval tool. The central claim is that this system automatically resolved an open problem in commutative algebra, producing a formally verified Lean 4 proof with essentially no human involvement.

Significance. If substantiated, the result would be significant for automated mathematical reasoning, as it provides a concrete instantiation of informal-formal collaboration that reduces human effort on research-level problems while ensuring machine-checkable correctness. The use of theorem retrieval for cross-domain technique discovery is a promising direction, and the emphasis on autonomous gap-filling by the formal agent addresses a key bottleneck in LLM-based proof generation.

major comments (2)

[Abstract and §4] Abstract and §4 (Case Study): The claim that the framework resolved an open commutative algebra problem with 'essentially no human involvement' is not accompanied by the explicit statement of the conjecture, the informal proof sketch generated by Rethlas, the specific gaps encountered, the number of refinement rounds, or any success metrics (e.g., fraction of tactics auto-synthesized). Without these details it is impossible to assess whether Archon truly closed nontrivial gaps autonomously or whether the informal output was already nearly formalizable.
[§5] §5 (Experiments): The reported experiments on theorem retrieval strength do not include quantitative results for the commutative algebra instance, such as iteration counts, error rates in LeanSearch synthesis, or a comparison against baselines with human-written lemmas. This leaves the assertion that 'the formal agent is capable of autonomously filling nontrivial gaps' without load-bearing evidence.

minor comments (2)

[Figure 1] The architecture diagram (Figure 1) does not clearly distinguish the interfaces between Matlas and LeanSearch or show the exact data flow from informal output to Lean project initialization.
Notation for the two agents is introduced without reference to prior naming conventions in the LLM-for-math literature, which may confuse readers.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. We address each major comment below and will revise the manuscript to incorporate additional details and evidence as requested.

read point-by-point responses

Referee: [Abstract and §4] Abstract and §4 (Case Study): The claim that the framework resolved an open commutative algebra problem with 'essentially no human involvement' is not accompanied by the explicit statement of the conjecture, the informal proof sketch generated by Rethlas, the specific gaps encountered, the number of refinement rounds, or any success metrics (e.g., fraction of tactics auto-synthesized). Without these details it is impossible to assess whether Archon truly closed nontrivial gaps autonomously or whether the informal output was already nearly formalizable.

Authors: We agree that the current version of the abstract and §4 would benefit from greater explicitness to allow independent assessment of the autonomy claim. In the revised manuscript we will add: (i) the precise statement of the open commutative-algebra conjecture, (ii) the full informal proof sketch produced by Rethlas, (iii) a description of the specific gaps that Archon encountered, (iv) the exact number of refinement rounds performed, and (v) quantitative success metrics (including the fraction of tactics auto-synthesized by LeanSearch). These additions will make the division of labor between the two agents transparent and will directly support the assertion of minimal human involvement. revision: yes
Referee: [§5] §5 (Experiments): The reported experiments on theorem retrieval strength do not include quantitative results for the commutative algebra instance, such as iteration counts, error rates in LeanSearch synthesis, or a comparison against baselines with human-written lemmas. This leaves the assertion that 'the formal agent is capable of autonomously filling nontrivial gaps' without load-bearing evidence.

Authors: We concur that instance-specific quantitative data are necessary to substantiate the claim. The revised §5 will include, for the commutative-algebra case study: iteration counts, observed error rates during LeanSearch-assisted synthesis, and a direct comparison against a baseline that supplies human-written lemmas. These metrics will provide concrete, load-bearing evidence that the formal agent autonomously closed nontrivial gaps. revision: yes

Circularity Check

0 steps flagged

No circularity: system architecture paper with empirical demonstration

full rationale

The paper presents a two-component framework (Rethlas informal agent using Matlas search + Archon formal agent using LeanSearch) whose central claim is an empirical demonstration that the system resolved one open commutative algebra conjecture and produced a Lean 4 proof with essentially no human intervention. No equations, fitted parameters, self-referential definitions, or load-bearing self-citations appear in the provided text; the work is an engineering description of an agent pipeline rather than a derivation that reduces to its own inputs by construction. The resolution is offered as an existence proof of the framework's capability, not as a result derived from the framework's own prior outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claim depends on the unproven assumption that current large language models, when augmented with theorem search, can generate informal arguments sufficiently structured for reliable formalization; no free parameters or new physical entities are introduced.

axioms (1)

domain assumption Large language models combined with theorem retrieval can produce usable informal mathematical arguments for research-level problems.
Invoked to justify the informal reasoning agent Rethlas.

invented entities (2)

Rethlas informal reasoning agent no independent evidence
purpose: Combines reasoning primitives with Matlas theorem search to explore solution strategies.
New system component introduced by the paper.
Archon formal verification agent no independent evidence
purpose: Translates informal arguments into Lean 4 projects via task decomposition and automated proof synthesis.
New system component introduced by the paper.

pith-pipeline@v0.9.0 · 5610 in / 1294 out tokens · 85268 ms · 2026-05-13T18:01:26.433059+00:00 · methodology

discussion (0)

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
cs.IR 2026-05 conditional novelty 7.0

LeanSearch v2 recovers 46.1% of ground-truth premise groups on research-level Mathlib theorems and raises fixed-loop proof success from 4% to 20% via embedding-reranker plus iterative sketch-retrieve-reflect retrieval.
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
cs.IR 2026-05 conditional novelty 7.0

LeanSearch v2 recovers 46.1% of ground-truth premise groups for research-level Lean 4 theorems within 10 candidates and raises fixed-loop proof success to 20%.
Matlas: A Semantic Search Engine for Mathematics
cs.IR 2026-04 unverdicted novelty 7.0

Matlas introduces a semantic retrieval system over 8.07 million mathematical statements from papers and textbooks, using dependency graphs and topological unfolding for self-contained search via natural language queries.
Grokability in five inequalities
math.PR 2026-05 unverdicted novelty 5.0

Five improved inequalities were found with AI help: better Gaussian perimeter bounds for convex sets, sharper L2-L1 moments on the Hamming cube, a strengthened autoconvolution inequality, improved g-Sidon set bounds, ...

Reference graph

Works this paper leans on

59 extracted references · 59 canonical work pages · cited by 3 Pith papers · 5 internal anchors

[1]

Abouzaid, A

Mohammed Abouzaid, Andrew J Blumberg, Martin Hairer, Joe Kileel, Tamara G Kolda, Paul D Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, et al. First Proof.arXiv preprintarXiv:2602.05192, 2026

work page arXiv 2026
[2]

GPT-4 Technical Report

Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. GPT-4 Technical Report.arXiv preprint arXiv:2303.08774, 2023

work page internal anchor Pith review Pith/arXiv arXiv 2023
[3]

Aristotle: IMO-level Automated Theorem Proving

Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, et al. Aristotle: Imo-level automated theorem proving. arXiv preprint arXiv:2510.01346, 2025

work page internal anchor Pith review arXiv 2025
[4]

Quasi-complete semilocal rings and modules

Daniel D Anderson. Quasi-complete semilocal rings and modules. InCommutative Algebra: Recent Advancesin Commutative Rings, Integer-ValuedPolynomials, and Polynomial Functions, pages 25–37. Springer, 2014

work page 2014
[5]

Irrationality of rapidly converging series: a problem of erd\h{o}s and graham.arXiv preprint arXiv:2601.21442, 2026

Kevin Barreto, Jiwon Kang, Sang-hyun Kim, Vjekoslav Kovač, and Shengtong Zhang. Irrationality of rapidly converging series: a problem of erd\h{o}s and graham.arXiv preprint arXiv:2601.21442, 2026

work page arXiv 2026
[6]

Ax-prover: A deep reasoning agentic framework for theorem proving in mathematics and quantum physics.arXiv preprint arXiv:2510.12787, 2025

Benjamin Breen, Marco Del Tredici, Jacob McCarran, Javier Aspuru Mijares, Weichen Winston Yin, Kfir Sulimany, Jacob M Taylor, Frank HL Koppens, and Dirk Englund. Ax-prover: A deep reasoning agentic framework for theorem proving in mathematics and quantum physics.arXiv preprint arXiv:2510.12787, 2025

work page arXiv 2025
[7]

The motivic class of the space of genus0maps to the flag variety.arXiv preprint arXiv:2601.07222, 2026

Jim Bryan, Balázs Elek, Freddie Manners, George Salafatinos, and Ravi Vakil. The motivic class of the space of genus0maps to the flag variety.arXiv preprint arXiv:2601.07222, 2026

work page arXiv 2026
[8]

Open problems in commutative ring theory

Paul-Jean Cahen, Marco Fontana, Sophie Frisch, and Sarah Glaz. Open problems in commutative ring theory. In CommutativeAlgebra: Recent Advancesin CommutativeRings, Integer-ValuedPolynomials, and Polynomial Functions, pages 353–375. Springer, 2014

work page 2014
[9]

Fel’s conjecture on syzygies of numerical semigroups, 2026.https://arxiv.org/abs/2602.03716

Evan Chen, Chris Cummins, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, et al. Fel’s conjecture on syzygies of numerical semigroups.arXiv preprint arXiv:2602.03716, 2026

work page arXiv 2026
[10]

Seed-prover 1.5: Mastering undergraduate-level theorem proving via learning from experience.arXiv preprint arXiv:2512.17260,

Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, et al. Seed-prover 1.5: Mastering undergraduate-level theorem proving via learning from experience. arXiv preprint arXiv:2512.17260, 2025

work page arXiv 2025
[11]

On the theory of local rings.Annals of Mathematics, 44(4):690–708, 1943

Claude Chevalley. On the theory of local rings.Annals of Mathematics, 44(4):690–708, 1943

work page 1943
[12]

Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities

Gheorghe Comanici, Eric Bieber, Mike Schaekermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, et al. Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities.arXiv preprint arXiv:2507.06261, 2025

work page internal anchor Pith review Pith/arXiv arXiv 2025
[13]

open problems in commutative ring theory

Jonathan David Farley. Quasi-completeness and localizations of polynomial domains: A conjecture from “open problems in commutative ring theory”.Bulletin of the Korean Mathematical Society, 53(6):1613–1615, 2016

work page 2016
[14]

Eigenweights for arithmetic hirzebruch proportionality.arXiv preprint arXiv:2601.23245, 2026

Tony Feng. Eigenweights for arithmetic hirzebruch proportionality.arXiv preprint arXiv:2601.23245, 2026

work page arXiv 2026
[15]

Aletheia tackles FirstProof autonomously.arXiv preprint arXiv:2602.21201, 2026

Tony Feng, Junehyuk Jung, Sang-hyun Kim, Carlo Pagano, Sergei Gukov, Chiang-Chiang Tsai, David Woodruff, Adel Javanmard, Aryan Mokhtari, Dawsen Hwang, et al. Aletheia tackles FirstProof autonomously.arXiv preprint arXiv:2602.21201, 2026

work page arXiv 2026
[16]

Semi-autonomous mathematics discovery with gemini: A case study on the erd\h{o}s problems

Tony Feng, Trieu Trinh, Garrett Bingham, Jiwon Kang, Shengtong Zhang, Sang-hyun Kim, Kevin Barreto, Carl Schildkraut, Junehyuk Jung, Jaehyeon Seo, et al. Semi-autonomous mathematics discovery with gemini: A case study on the erd\h{o}s problems. arXiv preprint arXiv:2601.22401, 2026

work page arXiv 2026
[17]

Towards Autonomous Mathematics Research.arXiv preprint arXiv:2602.10177, 2026

Tony Feng, Trieu H Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung, Joonkyung Lee, Carlo Pagano, Sang-hyun Kim, Federico Pasqualotto, et al. Towards Autonomous Mathematics Research.arXiv preprint arXiv:2602.10177, 2026

work page arXiv 2026
[18]

Completely controlling the dimensions of formal fiber rings at prime ideals of small height.Journal of Commutative Algebra, 11(3):363–388, 2019

Sarah M Fleming, Lena Ji, Susan Loepp, Peter M McDonald, Nina Pande, and David Schwein. Completely controlling the dimensions of formal fiber rings at prime ideals of small height.Journal of Commutative Algebra, 11(3):363–388, 2019. 15

work page 2019
[19]

A semantic search engine for mathlib4

Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for mathlib4. In Findings of the Association for Computational Linguistics: EMNLP 2024, pages 8001–8013, 2024

work page 2024
[20]

A semantic search engine for mathlib4

Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset.arXiv preprint arXiv:2410.10878, 2024

work page arXiv 2024
[21]

FrontierMath: A benchmark for evaluating advanced mathematical reasoning in AI.arXiv preprint arXiv:2411.04872, 2024

Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Caroline Falkman Olsson, Jean-Stanislas Denain, Anson Ho, Emily de Oliveira Santos, et al. Frontiermath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI.arXiv preprint arXiv:2411.04872, 2024

work page arXiv 2024
[22]

DeepSeek-R1 Incentivizes Reasoning in LLMs Through Reinforcement Learning.Nature, 645 (8081):633–638, 2025

Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Peiyi Wang, Qihao Zhu, Runxin Xu, Ruoyu Zhang, Shirong Ma, Xiao Bi, et al. DeepSeek-R1 Incentivizes Reasoning in LLMs Through Reinforcement Learning.Nature, 645 (8081):633–638, 2025

work page 2025
[23]

Characterization of completions of unique factorization domains.Transactions of the American Mathematical Society, 337(1):379–387, 1993

Raymond C Heitmann. Characterization of completions of unique factorization domains.Transactions of the American Mathematical Society, 337(1):379–387, 1993

work page 1993
[24]

biology" or

Yichen Huang and Lin F Yang. Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline. arXiv preprint arXiv:2507.15855, 2025

work page arXiv 2025
[25]

Olympiad-level formal mathematical reasoning with reinforcement learning.Nature, pages 1–3, 2025

Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, et al. Olympiad-level formal mathematical reasoning with reinforcement learning.Nature, pages 1–3, 2025

work page 2025
[26]

Semi-autonomous formalization of the vlasov-maxwell-landau equilibrium

Vasily Ilin. Semi-autonomous formalization of the vlasov-maxwell-landau equilibrium. arXiv preprint arXiv:2603.15929, 2026

work page arXiv 2026
[27]

Completions of ufds with semi-local formal fibers.Communications in Algebra®, 34(1):347–360, 2006

David Jensen. Completions of ufds with semi-local formal fibers.Communications in Algebra®, 34(1):347–360, 2006

work page 2006
[28]

Jiang, W

Jiedong Jiang, Wanyi He, Yuefeng Wang, Guoxiong Gao, Yongle Hu, Jingting Wang, Nailing Guan, Peihao Wu, Chunbo Dai, Liang Xiao, et al. FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels. arXiv preprint arXiv:2511.02872, 2025

work page arXiv 2025
[29]

AI for Mathematics: Progress, Challenges, and Prospects

Haocheng Ju and Bin Dong. Ai for mathematics: Progress, challenges, and prospects. arXiv preprint arXiv:2601.13209, 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026
[30]

Comparator: A trustworthy judge for lean proof submissions

Lean Community. Comparator: A trustworthy judge for lean proof submissions. https://github.com/ leanprover/comparator, 2025. GitHub repository

work page 2025
[31]

Lower bounds for multivariate independence polynomials and their generalisa- tions

Joonkyung Lee and Jaehyeon Seo. Lower bounds for multivariate independence polynomials and their generalisa- tions. arXiv preprint arXiv:2602.02450, 2026

work page arXiv 2026
[32]

Numina-lean-agent: An open and general agentic reasoning system for formal mathematics.arXiv preprint arXiv:2601.14027,

Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, et al. Numina-lean-agent: An open and general agentic reasoning system for formal mathematics. arXiv preprint arXiv:2601.14027, 2026

work page arXiv 2026
[33]

Constructing local generic formal fibers.Journal of Algebra, 187(1):16–38, 1997

S Loepp. Constructing local generic formal fibers.Journal of Algebra, 187(1):16–38, 1997

work page 1997
[34]

Completing the formal proof of higher-dimensional sphere packing

Math, Inc. Completing the formal proof of higher-dimensional sphere packing. https://math.inc/ sphere-packing, 2026. Blog post

work page 2026
[35]

Leanstral: Open-source foundation for trustworthy vibe-coding

Mistral AI. Leanstral: Open-source foundation for trustworthy vibe-coding. https://mistral.ai/news/ leanstral, March 2026. Blog post

work page 2026
[36]

First Proof? Technical report, OpenAI, February 2026

OpenAI. First Proof? Technical report, OpenAI, February 2026. URL https://cdn.openai.com/pdf/ 26177a73-3b75-4828-8c91-e8f1cf27aaa0/oai_first_proof.pdf. OpenAI First Proof submissions

work page 2026
[37]

The simplicity of the hodge bundle.arXiv preprint arXiv:2603.19052, 2026

Anand Patel. The simplicity of the hodge bundle.arXiv preprint arXiv:2603.19052, 2026

work page arXiv 2026
[38]

QwQ-32B: Embracing the Power of Reinforcement Learning, March 2025

Qwen Team. QwQ-32B: Embracing the Power of Reinforcement Learning, March 2025. URLhttps://qwenlm. github.io/blog/qwq-32b/

work page 2025
[39]

Aria: An agent for retrieval and iterative auto-formalization via dependency graph.arXiv preprint arXiv:2510.04520, 2025

Hanyu Wang, Ruohan Xie, Yutong Wang, Guoxiong Gao, Xintao Yu, and Bin Dong. Aria: An agent for retrieval and iterative auto-formalization via dependency graph.arXiv preprint arXiv:2510.04520, 2025

work page arXiv 2025
[40]

Qwen3 Technical Report

An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, et al. Qwen3 Technical Report.arXiv preprint arXiv:2505.09388, 2025. 16 Appendix A Mathematical Proof of Anderson’s Conjecture In this section, we present the mathematical construction and proof of Anderson’s conjecture as generated and v...

work page internal anchor Pith review Pith/arXiv arXiv 2025
[41]

IfRis complete with respect to theM-adic topology, thenRis quasi-complete [11, Lemma 7]

work page
[42]

3.R is quasi-complete if and only if every homomorphic imageR/I (for any proper idealI) is weakly quasi-complete [4, Theorem 1.3]

IfRis quasi-complete, thenRis weakly quasi-complete. 3.R is quasi-complete if and only if every homomorphic imageR/I (for any proper idealI) is weakly quasi-complete [4, Theorem 1.3]. The main result of this section provides a negative answer to Anderson’s question. Theorem 6.There exists a weakly quasi-complete Noetherian local ring that is not quasi-com...

work page
[43]

Proof.The ringC[[x, y, z]]is a complete regular local domain of dimension3

The height-one prime idealQ= (x, y)Tis not principal. Proof.The ringC[[x, y, z]]is a complete regular local domain of dimension3. The quotient T=C[[x, y, z]]/(x 2 −yz) is isomorphic to the subringC[[u2, uv, v2]]⊆C[[u, v]]via x7→uv, y7→u 2, z7→v 2. Hence T is a domain. Sincex2 −yz is a nonzerodivisor in the regular local ringC[[x, y, z]], the quotientT is ...

work page
[44]

4.P= (0)is nonmaximal and meets the prime subring trivially

SinceTis a domain, its only associated prime is(0), soP= (0)contains all associated primes. 4.P= (0)is nonmaximal and meets the prime subring trivially

work page
[45]

Therefore Jensen’s corollary yields a local UFDA with bA ∼= T whose generic formal fiber is local with maximal ideal(0)

BecauseTis Cohen–Macaulay, there is no primeJwithht(J)>depth(T J ) = 1. Therefore Jensen’s corollary yields a local UFDA with bA ∼= T whose generic formal fiber is local with maximal ideal(0). Verification thatAis the desired counterexample By Theorem 10, the generic formal fiber ofA is trivial: the only prime ideal ofbA ∼= T contracting to(0)in A is(0)it...

work page
[46]

\(T\) is a complete \(2\)-dimensional Cohen-Macaulay local domain

work page
[47]

\(|T|=|T/M|=|\mathbb{C}|\)

work page
[48]

## proof The ring \(\mathbb{C}[[x,y,z]]\) is a complete regular local domain of dimension \(3\)

The height-one prime ideal \[ Q=(x,y)T \] is not principal. ## proof The ring \(\mathbb{C}[[x,y,z]]\) is a complete regular local domain of dimension \(3\). The quotient \[ T=\mathbb{C}[[x,y,z]]/(x^2-yz) \] is isomorphic to the subring \(\mathbb{C}[[u^2,uv,v^2]]\subseteq \mathbb{C}[[u,v]]\) via \[ x\mapsto uv,\qquad y\mapsto u^2,\qquad z\mapsto v^2. \] He...

work page doi:10.1080/00927870500346321
[49]

\(P\) is nonmaximal and contains all associated prime ideals of \(T\)

work page
[50]

\(P\cap\) the prime subring of \(T\) is \((0)\)

work page
[51]

The hypotheses hold:

if \(J\in \operatorname{Spec}T\) with \(\operatorname{ht}(J)>\operatorname{depth}(T_J) =1\), then \(J\subseteq P\).” We apply this with the ring \(T\) from Lemma \ref{lem:complete_domain_choice} and with \(P=(0)\). The hypotheses hold:

work page
[52]

\(T\) is complete and \(|T|=|T/M|\) by Lemma \ref{lem:complete_domain_choice}

work page
[53]

\(T\) has depth \(2\) by Lemma \ref{lem:complete_domain_choice}

work page
[54]

Since \(T\) is a domain, its only associated prime is \((0)\), so \(P=(0)\) contains all associated primes

work page
[55]

\(P=(0)\) is nonmaximal and meets the prime subring trivially

work page
[56]

Therefore Jensen’s corollary yields a local UFD \(A\) with \(\widehat A\cong T\) whose generic formal fiber is local with maximal ideal \((0)\)

Because \(T\) is Cohen-Macaulay, there is no prime \(J\) with \(\operatorname{ht}(J)> \operatorname{depth}(T_J)=1\). Therefore Jensen’s corollary yields a local UFD \(A\) with \(\widehat A\cong T\) whose generic formal fiber is local with maximal ideal \((0)\). # lemma lem:a_is_weak_and_has_bad_quotient ## statement For the ring \(A\) of Lemma \ref{lem:je...

work page
[57]

\(A\) is weakly quasi-complete

work page
[58]

Open Problems in Commutative Ring Theory

There exists a prime element \(a\in A\) such that \(A/aA\) is a one-dimensional Noetherian local domain that is not weakly quasi-complete. ## proof Because the generic formal fiber of \(A\) is local with maximal ideal \((0)\), the only prime ideal of \(\widehat A\cong T\) contracting to \((0)\) is \((0)\) itself. Hence every nonzero prime ideal of \(\wide...

work page 2014
[59]

A Noetherian local ring \(R\) is quasi-complete if and only if each homomorphic image of \(R\) is weakly quasi-complete

[4] D. D. Anderson, Quasi-complete semilocal rings and modules, Commutative Algebra: Recent Advances in Commutative Rings, Integer-Valued Polynomials, and Polynomial Functions, Springer Verlag, New York, 2014. Prove that there exists a weakly quasi-complete ring that is not quasi-complete. ## proof Let \(A\) be the local UFD constructed in Lemma \ref{lem:...

work page 2014