Automated Conjecture Resolution with Formal Verification
DOI:
https://doi.org/10.70777/si.v3i3.18746Keywords:
automated conjecture resolution, formal verification, mathematical reasoning, Lean 4, theorem retrieval, Rethlas, Archon, Matlas, LeanSearch, research-level mathematicsAbstract
Recent advances in large language models (LLMs) 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 mathematical 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 fully 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 proposed by D. D. Anderson (2014) and formally verify the resulting proof in Lean 4 with essentially no human involvement. Additional research-level case studies further 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 deep, 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 with minimal human involvement.
References
[1] Ahmed Abbes, Michel Gros, and Takeshi Tsuji. The p-adic Simpson correspondence, volume 193. Princeton University Press, 2016.
[2] 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 preprint arXiv:2602.05192, 2026.
[3] 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.
[4] 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.
[5] Daniel D Anderson. Quasi-complete semilocal rings and modules. In Commutative Algebra: Recent Advances in Commutative Rings, Integer-Valued Polynomials, and Polynomial Functions, pages 25–37. Springer, 2014.
[6] Johannes Anschütz, Ben Heuer, and Arthur-César Le Bras. The small p-adic simpson correspondence in terms of moduli spaces. arXiv preprint arXiv:2312.07554, 2023.
[7] Kevin Barreto, Jiwon Kang, Sang-hyun Kim, Vjekoslav Kovač, and Shengtong Zhang. Irrationality of rapidly converging series: a problem of erdh {o} s and graham. arXiv preprint arXiv:2601.21442, 2026.
[8] 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.
[9] Haïm Brezis. Some of my favorite open problems. Atti Accad. Naz. Lincei Cl. Sci. Fis. Mat. Natur., 34(2):307–335, 2023. doi: 10.4171/RLM/1008.
[10] Jim Bryan, Balázs Elek, Freddie Manners, George Salafatinos, and Ravi Vakil. The motivic class of the space of genus 0 maps to the flag variety. arXiv preprint arXiv:2601.07222, 2026.
[11] Paul-Jean Cahen, Marco Fontana, Sophie Frisch, and Sarah Glaz. Open problems in commutative ring theory. In Commutative Algebra: Recent Advances in Commutative Rings, Integer-Valued Polynomials, and Polynomial Functions, pages 353–375. Springer, 2014.
[12] 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.
[13] 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.
[14] Claude Chevalley. On the theory of local rings. Annals of Mathematics, 44(4):690–708, 1943.
[15] 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.
[16] Brian Conrad. The structure of solvable groups over general fields. In Autour des schémas en groupes, volume 46 of Panoramas et Synthèses, pages 159–192. Société Mathématique de France, 2015.
[17] Brian Conrad and Gopal Prasad. Structure and classification of pseudo-reductive groups. In Algebraic Groups: Structure and Actions, volume 94 of Proceedings of Symposia in Pure Mathematics, pages 127–276. American Mathematical Society, 2017.
[18] Brian Conrad, Ofer Gabber, and Gopal Prasad. Pseudo-reductive Groups. New Mathematical Monographs. Cambridge University Press, 2 edition, 2015.
[19] Xu’an Dou and Zeyu Jin. Degenerate constants in degree inequalities for sobolev circle maps: on some problems posed by brezis, 2026. URL https://arxiv.org/abs/2605.24626. 21
[20] 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.
[21] Tony Feng. Eigenweights for arithmetic hirzebruch proportionality. arXiv preprint arXiv:2601.23245, 2026.
[22] 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.
[23] 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 erdh {o} s problems. arXiv preprint arXiv:2601.22401, 2026.
[24] 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.
[25] 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.
[26] 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.
[27] 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.
[28] 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.
[29] 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.
[30] Richard Hain. Remarks on non-abelian cohomology of proalgebraic groups. arXiv preprint arXiv:1009.3662, 2010.
[31] Raymond C Heitmann. Characterization of completions of unique factorization domains. Transactions of the American Mathematical Society, 337(1):379–387, 1993.
[32] 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.
[33] 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.
[34] Vasily Ilin. Semi-autonomous formalization of the vlasov-maxwell-landau equilibrium. arXiv preprint arXiv:2603.15929, 2026.
[35] David Jensen. Completions of ufds with semi-local formal fibers. Communications in Algebra®, 34(1):347–360, 2006.
[36] 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.
[37] Jiedong Jiang, Yixiao Li, Zeming Sun, Yuefeng Wang, Liang Xiao, and Jiahong Yu. On some open problems in commutative algebra resolved by rethlas, 2026. URL https://arxiv.org/abs/2605.25259.
[38] Haocheng Ju and Bin Dong. Ai for mathematics: Progress, challenges, and prospects. arXiv preprint arXiv:2601.13209, 2026.
[39] Aaron Landesman and Daniel Litt. Prill’s problem. Algebraic Geometry, 2024. doi: 10.14231/AG-2024-009. URL https://api.algebraicgeometry.nl/Article/20170/2024-2-009.pdf. 22
[40] Lean Community. Comparator: A trustworthy judge for lean proof submissions. https://github.com/ leanprover/comparator, 2025. GitHub repository.
[41] Joonkyung Lee and Jaehyeon Seo. Lower bounds for multivariate independence polynomials and their generalisa- tions. arXiv preprint arXiv:2602.02450, 2026.
[42] 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.
[43] S Loepp. Constructing local generic formal fibers. Journal of Algebra, 187(1):16–38, 1997.
[44] João Lourenço. Grassmanniennes affines tordues sur les entiers. arXiv preprint arXiv:1912.11918, 2019.
[45] Math, Inc. Completing the formal proof of higher-dimensional sphere packing. https://math.inc/ sphere-packing, 2026. Blog post.
[46] Yu Min and Yupeng Wang. Integral p-adic non-abelian hodge theory for small representations. Advances in Mathematics, 458:109950, 2024.
[47] Mistral AI. Leanstral: Open-source foundation for trustworthy vibe-coding. https://mistral.ai/news/ leanstral, March 2026. Blog post.
[48] Masayoshi Nagata. Local Rings. Interscience Tracts in Pure and Applied Mathematics, No. 13. Interscience Publishers, a division of John Wiley & Sons, New York–London, 1962.
[49] 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.
[50] Xiangyu Pan and Jiahong Yu. Lift-independence problem in the p-adic simpson correspondence for curves. arXiv preprint arXiv:2605.29947, 2026.
[51] Anand Patel. The simplicity of the hodge bundle. arXiv preprint arXiv:2603.19052, 2026.
[52] Zev Rosengarten. Pathological behavior of arithmetic invariants of unipotent groups. Algebra & Number Theory, 15(7):1593–1626, November 2021. ISSN 1937-0652. doi: 10.2140/ant.2021.15.1593. URL http://dx.doi.org/10. 2140/ant.2021.15.1593.
[53] Mao Sheng and Yupeng Wang. The small p-adic simpson correspondence in the semi-stable reduction case. arXiv preprint arXiv:2410.09685, 2024.
[54] Qwen Team. QwQ-32B: Embracing the Power of Reinforcement Learning, March 2025. URL https://qwenlm. github.io/blog/qwq-32b/.
[55] 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.
[56] 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. 23
Downloads
Published
How to Cite
Issue
Section
Categories
License
Copyright (c) 2026 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
This work is licensed under a Creative Commons Attribution 4.0 International License.
