---
title: "Automated Conjecture Resolution with Formal Verification (2026)"
description: "Large language models can now attempt research-level mathematics, but checking their… 56 references, cited by 5 papers here."
authors: ["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"]
year: 2026
venue: "arXiv:2604.03789"
source: "https://arxiv.org/abs/2604.03789"
doi: "10.48550/arxiv.2604.03789"
arxiv: "2604.03789"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/ju-2026-automated-conjecture-resolution-formal-verification/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/ju-2026-automated-conjecture-resolution-formal-verification/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2026](https://md.research.elamur.ai/free/en/papers/2026/page/3/) / Automated Conjecture Resolution with Formal Verification

# Automated Conjecture Resolution with Formal Verification

**Authors:** [Haocheng Ju](https://md.research.elamur.ai/free/en/authors/haocheng-ju/), [Guoxiong Gao](https://md.research.elamur.ai/free/en/authors/guoxiong-gao/), [Jiedong Jiang](https://md.research.elamur.ai/free/en/authors/jiedong-jiang/), [Bin Wu](https://md.research.elamur.ai/free/en/authors/bin-wu/), Zeming Sun, Shurui Liu, Leheng Chen, [Yutong Wang](https://md.research.elamur.ai/free/en/authors/yutong-wang/), Yuefeng Wang, [Zichen Wang](https://md.research.elamur.ai/free/en/authors/zichen-wang/), [Wanyi He](https://md.research.elamur.ai/free/en/authors/wanyi-he/), [Peihao Wu](https://md.research.elamur.ai/free/en/authors/peihao-wu/), Liang Xiao, Ruochuan Liu, [Bryan Dai](https://md.research.elamur.ai/free/en/authors/bryan-dai/) and [Bin Dong](https://md.research.elamur.ai/free/en/authors/bin-dong/) · **Year:** 2026 · **Venue:** [arXiv:2604.03789](https://md.research.elamur.ai/free/en/venues/superintelligence-robotics-safety-alignment/) ([SuperIntelligence - Robotics - Safety & Alignment 2026](https://md.research.elamur.ai/free/en/venues/superintelligence-robotics-safety-alignment/2026/)) · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2604.03789) · [PDF](https://arxiv.org/pdf/2604.03789) · [DOI 10.48550/arxiv.2604.03789](https://doi.org/10.48550/arxiv.2604.03789) · [arXiv 2604.03789](https://arxiv.org/abs/2604.03789) · [OpenAlex](https://openalex.org/W7151534166)

**Citations:** 0 citations (OpenAlex, 2026-10-14) · 5 in our library, of the 149,439 papers whose bibliographies we read

## Summary
Large language models can now attempt research-level mathematics, but checking their natural-language proofs is slow, needs experts, and can still let errors through. The authors pair informal reasoning with machine-checked formal proofs to address this. Their pipeline has two agents. Rethlas works like a mathematician exploring a problem: it generates and verifies candidate proofs, builds examples and counterexamples, and queries Matlas, a semantic search engine over mathematical theorems. Archon takes the resulting informal argument and turns it into a complete Lean 4 project. It plans and decomposes the work into lemmas, refines proofs iteratively, manages memory, and uses the LeanSearch retrieval tool. When formalization stalls, it can ask Rethlas for more detail or a different route. Using this setup, the team settled an open commutative-algebra question posed by D. D. Anderson in 2014 and produced a Lean proof with almost no human input. This suggests that retrieval-equipped informal agents working with formal agents can make AI-driven mathematical discovery both faster and trustworthy.

## Key points
- **Architecture and tools:** Rethlas handles informal reasoning with the Matlas theorem search engine. Archon handles formalization with LeanSearch and has a planning sub-agent and an execution sub-agent. All components are open-sourced under github.com/frenzymath.
- **Anderson problem:** Matlas surfaced a technical result by Jensen from a neighboring area, which was decisive for the proof. Archon filled nontrivial gaps left by the informal proof and the cited references. The resulting formalization passed the Comparator checker.
- **Algebraic groups test:** Rethlas proved an expert-level, apparently unpublished problem in algebraic groups, suggested by Brian Conrad. On the same problem, GPT-5.5 Pro (web interface) gave an entirely wrong proof.
- **p-adic Hodge theory test:** Rethlas proved conjectures proposed by humans. It also removed an unnecessary hypothesis, made a qualitative condition explicit, and built a counterexample showing a remaining condition is needed.
- **Archon's limits and remaining effort:** Archon formalized two further research-level proofs, one fully autonomously and one after a single-sentence hint. Its generated Lean code still departs from Mathlib naming and style conventions, so contributing it upstream would take extra human work.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Stanford University](https://md.research.elamur.ai/free/en/universities/stanford-university/) — University, Stanford, United States · 567 works · 335,189 citations
- [Peking University](https://md.research.elamur.ai/free/en/universities/peking-university/) — University, Beijing, China · 335 works · 43,759 citations
- [Kyoto University](https://md.research.elamur.ai/free/en/universities/kyoto-university/) — University, Kyoto, Japan · 43 works · 8,240 citations
- [Westlake University](https://md.research.elamur.ai/free/en/universities/westlake-university/) — University, Hangzhou, China · 60 works · 8,829 citations
- [Tianjin University](https://md.research.elamur.ai/free/en/universities/tianjin-university/) — University, Tianjin, China · 54 works · 1,164 citations
- [Great Bay University](https://md.research.elamur.ai/free/en/universities/great-bay-university/) — University, Dongguan, China · 5 works · 8 citations

Also on the byline: [Research Institute for Mathematical Sciences, Kyoto University](https://ror.org/03j30yc45).

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

## Cite

Cite as: 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 and Bin Dong. 2026. Automated Conjecture Resolution with Formal Verification. arXiv:2604.03789.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{ju2026automated,
  title = {{Automated Conjecture Resolution with Formal Verification}},
  author = {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 and Bin Dong},
  year = {2026},
  doi = {10.48550/arxiv.2604.03789},
  eprint = {2604.03789},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2604.03789}
}
```

- [← previous Attention Sinks in Diffusion Language Models](https://md.research.elamur.ai/free/en/papers/rulli-2026-attention-sinks-diffusion-language-models/)
- [next → Automatic Reviewers Fail to Detect Faulty Reasoning in Research Papers: A New Counterfactual Evaluation Framework](https://md.research.elamur.ai/free/en/papers/dycke-2026-automatic-reviewers-fail-detect-faulty/)
- [↑ back to papers of 2026](https://md.research.elamur.ai/free/en/papers/2026/page/3/)

## References

56 references, 10 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Ahmed Abbes, Michel Gros, and Takeshi Tsuji. The p-adic Simpson correspondence, volume 193. Princeton University Press, 2016. [find](https://scholar.google.com/scholar?q=Ahmed+Abbes%2C+Michel+Gros%2C+and+Takeshi+Tsuji%2E+The+p%2Dadic+Simpson+correspondence%2C+volume+193%2E+Princeton+University+Press%2C+2016%2E)
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. — [arXiv:2602.05192](https://arxiv.org/abs/2602.05192) [find](https://scholar.google.com/scholar?q=Mohammed+Abouzaid%2C+Andrew+J+Blumberg%2C+Martin+Hairer%2C+Joe+Kileel%2C+Tamara+G+Kolda%2C+Paul+D+Nelson%2C+Daniel+Spielman%2C+Nikhil+Srivastava%2C+Rachel+Ward%2C+Shmuel+Weinberger%2C+et+al%2E+First+Proof%2E+arXiv+preprint+a)
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](https://md.research.elamur.ai/free/en/papers/openai-2023-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](https://md.research.elamur.ai/free/en/papers/achim-2025-aristotle-imo-level-automated-theorem/). 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. [find](https://scholar.google.com/scholar?q=Daniel+D+Anderson%2E+Quasi%2Dcomplete+semilocal+rings+and+modules%2E+In+Commutative+Algebra%3A+Recent+Advances+in+Commutative+Rings%2C+Integer%2DValued+Polynomials%2C+and+Polynomial+Functions%2C+pages+25%E2%80%9337%2E+Springer)
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. — [arXiv:2312.07554](https://arxiv.org/abs/2312.07554) [find](https://scholar.google.com/scholar?q=Johannes+Ansch%C3%BCtz%2C+Ben+Heuer%2C+and+Arthur%2DC%C3%A9sar+Le+Bras%2E+The+small+p%2Dadic+simpson+correspondence+in+terms+of+moduli+spaces%2E+arXiv+preprint+arXiv%3A2312%2E07554%2C+2023%2E+%E2%80%94+%5BarXiv%3A2312%2E07554%5D%28https%3A%2F%2Farxiv%2Eorg)
7. 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. — [arXiv:2601.21442](https://arxiv.org/abs/2601.21442) [find](https://scholar.google.com/scholar?q=Kevin+Barreto%2C+Jiwon+Kang%2C+Sang%2Dhyun+Kim%2C+Vjekoslav+Kova%C4%8D%2C+and+Shengtong+Zhang%2E+Irrationality+of+rapidly+converging+series%3A+a+problem+of+erd%5C%5Ch+%7Bo%7D+s+and+graham%2E+arXiv+preprint+arXiv%3A2601%2E21442%2C+2026%2E)
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](https://md.research.elamur.ai/free/en/papers/breen-2025-ax-prover-deep-reasoning-agentic/). arXiv preprint arXiv:2510.12787, 202…
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. — [doi:10.4171/rlm/1008](https://doi.org/10.4171/rlm/1008) [find](https://scholar.google.com/scholar?q=Ha%C3%AFm+Brezis%2E+Some+of+my+favorite+open+problems%2E+Atti+Accad%2E+Naz%2E+Lincei+Cl%2E+Sci%2E+Fis%2E+Mat%2E+Natur%2E%2C+34%282%29%3A307%E2%80%93335%2C+2023%2E+doi%3A+10%2E4171%2FRLM%2F1008%2E+%E2%80%94+%5Bdoi%3A10%2E4171%2Frlm%2F1008%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E4171%2Frlm%2F1008)
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. — [arXiv:2601.07222](https://arxiv.org/abs/2601.07222) [find](https://scholar.google.com/scholar?q=Jim+Bryan%2C+Bal%C3%A1zs+Elek%2C+Freddie+Manners%2C+George+Salafatinos%2C+and+Ravi+Vakil%2E+The+motivic+class+of+the+space+of+genus+0+maps+to+the+flag+variety%2E+arXiv+preprint+arXiv%3A2601%2E07222%2C+2026%2E+%E2%80%94+%5BarXiv%3A2601%2E07)
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. [find](https://scholar.google.com/scholar?q=Paul%2DJean+Cahen%2C+Marco+Fontana%2C+Sophie+Frisch%2C+and+Sarah+Glaz%2E+Open+problems+in+commutative+ring+theory%2E+In+Commutative+Algebra%3A+Recent+Advances+in+Commutative+Rings%2C+Integer%2DValued+Polynomials%2C+and+P)
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. — [arXiv:2602.03716](https://arxiv.org/abs/2602.03716) [find](https://scholar.google.com/scholar?q=Evan+Chen%2C+Chris+Cummins%2C+Dejan+Grubisic%2C+Leopold+Haller%2C+Letong+Hong%2C+Andranik+Kurghinyan%2C+Kenny+Lau%2C+Hugh+Leather%2C+Seewoo+Lee%2C+Aram+Markosyan%2C+et+al%2E+Fel%E2%80%99s+conjecture+on+syzygies+of+numerical+semigr)
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](https://md.research.elamur.ai/free/en/papers/chen-2025-seed-prover-1-5/). arXiv preprint arXiv:2512.17260, 2025.
14. Claude Chevalley. On the theory of local rings. Annals of Mathematics, 44(4):690–708, 1943. [find](https://scholar.google.com/scholar?q=Claude+Chevalley%2E+On+the+theory+of+local+rings%2E+Annals+of+Mathematics%2C+44%284%29%3A690%E2%80%93708%2C+1943%2E)
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](https://md.research.elamur.ai/free/en/papers/comanici-2025-gemini-2-5-pushing-frontier/). arXiv preprint a…
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. [find](https://scholar.google.com/scholar?q=Brian+Conrad%2E+The+structure+of+solvable+groups+over+general+fields%2E+In+Autour+des+sch%C3%A9mas+en+groupes%2C+volume+46+of+Panoramas+et+Synth%C3%A8ses%2C+pages+159%E2%80%93192%2E+Soci%C3%A9t%C3%A9+Math%C3%A9matique+de+France%2C+2015%2E)
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. [find](https://scholar.google.com/scholar?q=Brian+Conrad+and+Gopal+Prasad%2E+Structure+and+classification+of+pseudo%2Dreductive+groups%2E+In+Algebraic+Groups%3A+Structure+and+Actions%2C+volume+94+of+Proceedings+of+Symposia+in+Pure+Mathematics%2C+pages+127%E2%80%93)
18. Brian Conrad, Ofer Gabber, and Gopal Prasad. Pseudo-reductive Groups. New Mathematical Monographs. Cambridge University Press, 2 edition, 2015. [find](https://scholar.google.com/scholar?q=Brian+Conrad%2C+Ofer+Gabber%2C+and+Gopal+Prasad%2E+Pseudo%2Dreductive+Groups%2E+New+Mathematical+Monographs%2E+Cambridge+University+Press%2C+2+edition%2C+2015%2E)
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. — [arXiv:2605.24626](https://arxiv.org/abs/2605.24626) [↗](https://arxiv.org/abs/2605.24626)
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. [find](https://scholar.google.com/scholar?q=Jonathan+David+Farley%2E+Quasi%2Dcompleteness+and+localizations+of+polynomial+domains%3A+A+conjecture+from+%E2%80%9Copen+problems+in+commutative+ring+theory%E2%80%9D%2E+Bulletin+of+the+Korean+Mathematical+Society%2C+53%286%29%3A1613)
21. Tony Feng. Eigenweights for arithmetic hirzebruch proportionality. arXiv preprint arXiv:2601.23245, 2026. — [arXiv:2601.23245](https://arxiv.org/abs/2601.23245) [find](https://scholar.google.com/scholar?q=Tony+Feng%2E+Eigenweights+for+arithmetic+hirzebruch+proportionality%2E+arXiv+preprint+arXiv%3A2601%2E23245%2C+2026%2E+%E2%80%94+%5BarXiv%3A2601%2E23245%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2601%2E23245%29)
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. [find](https://scholar.google.com/scholar?q=Tony+Feng%2C+Junehyuk+Jung%2C+Sang%2Dhyun+Kim%2C+Carlo+Pagano%2C+Sergei+Gukov%2C+Chiang%2DChiang+Tsai%2C+David+Woodruff%2C+Adel+Javanmard%2C+Aryan+Mokhtari%2C+Dawsen+Hwang%2C+et+al%2E+Aletheia+tackles+FirstProof+autonomously%2E+)
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 erd\\h {o} s problems. arXiv preprint arXiv:2601.22401, 2026. [find](https://scholar.google.com/scholar?q=Tony+Feng%2C+Trieu+Trinh%2C+Garrett+Bingham%2C+Jiwon+Kang%2C+Shengtong+Zhang%2C+Sang%2Dhyun+Kim%2C+Kevin+Barreto%2C+Carl+Schildkraut%2C+Junehyuk+Jung%2C+Jaehyeon+Seo%2C+et+al%2E+Semi%2Dautonomous+mathematics+discovery+with+gem)
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. [find](https://scholar.google.com/scholar?q=Tony+Feng%2C+Trieu+H+Trinh%2C+Garrett+Bingham%2C+Dawsen+Hwang%2C+Yuri+Chervonyi%2C+Junehyuk+Jung%2C+Joonkyung+Lee%2C+Carlo+Pagano%2C+Sang%2Dhyun+Kim%2C+Federico+Pasqualotto%2C+et+al%2E+Towards+Autonomous+Mathematics+Research)
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. [find](https://scholar.google.com/scholar?q=Sarah+M+Fleming%2C+Lena+Ji%2C+Susan+Loepp%2C+Peter+M+McDonald%2C+Nina+Pande%2C+and+David+Schwein%2E+Completely+controlling+the+dimensions+of+formal+fiber+rings+at+prime+ideals+of+small+height%2E+Journal+of+Commutat)
26. Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. [A semantic search engine for mathlib4](https://md.research.elamur.ai/free/en/papers/gao-2024-semantic-search-engine-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](https://md.research.elamur.ai/free/en/papers/gao-2024-herald-natural-language-annotated-lean/). 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](https://md.research.elamur.ai/free/en/papers/glazer-2024-frontiermath-benchmark-evaluating-advanced-mathematical/). 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. [find](https://scholar.google.com/scholar?q=Daya+Guo%2C+Dejian+Yang%2C+Haowei+Zhang%2C+Junxiao+Song%2C+Peiyi+Wang%2C+Qihao+Zhu%2C+Runxin+Xu%2C+Ruoyu+Zhang%2C+Shirong+Ma%2C+Xiao+Bi%2C+et+al%2E+DeepSeek%2DR1+Incentivizes+Reasoning+in+LLMs+Through+Reinforcement+Learning%2E)
30. Richard Hain. Remarks on non-abelian cohomology of proalgebraic groups. arXiv preprint arXiv:1009.3662, 2010. — [arXiv:1009.3662](https://arxiv.org/abs/1009.3662) [find](https://scholar.google.com/scholar?q=Richard+Hain%2E+Remarks+on+non%2Dabelian+cohomology+of+proalgebraic+groups%2E+arXiv+preprint+arXiv%3A1009%2E3662%2C+2010%2E+%E2%80%94+%5BarXiv%3A1009%2E3662%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1009%2E3662%29)
31. Raymond C Heitmann. Characterization of completions of unique factorization domains. Transactions of the American Mathematical Society, 337(1):379–387, 1993. [find](https://scholar.google.com/scholar?q=Raymond+C+Heitmann%2E+Characterization+of+completions+of+unique+factorization+domains%2E+Transactions+of+the+American+Mathematical+Society%2C+337%281%29%3A379%E2%80%93387%2C+1993%2E)
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. — [arXiv:2507.15855](https://arxiv.org/abs/2507.15855) [find](https://scholar.google.com/scholar?q=Yichen+Huang+and+Lin+F+Yang%2E+Winning+Gold+at+IMO+2025+with+a+Model%2DAgnostic+Verification%2Dand%2DRefinement+Pipeline%2E+arXiv+preprint+arXiv%3A2507%2E15855%2C+2025%2E+%E2%80%94+%5BarXiv%3A2507%2E15855%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2507)
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. [find](https://scholar.google.com/scholar?q=Thomas+Hubert%2C+Rishi+Mehta%2C+Laurent+Sartran%2C+Mikl%C3%B3s+Z+Horv+%C3%A1th%2C+Goran+%C5%BDu%C5%BEi%C4%87%2C+Eric+Wieser%2C+Aja+Huang%2C+Julian+Schrittwieser%2C+Yannick+Schroecker%2C+Hussain+Masoom%2C+et+al%2E+Olympiad%2Dlevel+formal+mathematical)
34. Vasily Ilin. Semi-autonomous formalization of the vlasov-maxwell-landau equilibrium. arXiv:2603.15929, 2026. arXiv preprint — [arXiv:2603.15929](https://arxiv.org/abs/2603.15929) [find](https://scholar.google.com/scholar?q=Vasily+Ilin%2E+Semi%2Dautonomous+formalization+of+the+vlasov%2Dmaxwell%2Dlandau+equilibrium%2E+arXiv%3A2603%2E15929%2C+2026%2E+arXiv+preprint+%E2%80%94+%5BarXiv%3A2603%2E15929%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2603%2E15929%29)
35. David Jensen. Completions of ufds with semi-local formal fibers. Communications in Algebra®, 34(1):347–360, 2006. [find](https://scholar.google.com/scholar?q=David+Jensen%2E+Completions+of+ufds+with+semi%2Dlocal+formal+fibers%2E+Communications+in+Algebra%C2%AE%2C+34%281%29%3A347%E2%80%93360%2C+2006%2E)
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. — [arXiv:2511.02872](https://arxiv.org/abs/2511.02872) [find](https://scholar.google.com/scholar?q=Jiedong+Jiang%2C+Wanyi+He%2C+Yuefeng+Wang%2C+Guoxiong+Gao%2C+Yongle+Hu%2C+Jingting+Wang%2C+Nailing+Guan%2C+Peihao+Wu%2C+Chunbo+Dai%2C+Liang+Xiao%2C+et+al%2E+FATE%3A+A+Formal+Benchmark+Series+for+Frontier+Algebra+of+Multiple+)
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. — [arXiv:2605.25259](https://arxiv.org/abs/2605.25259) [↗](https://arxiv.org/abs/2605.25259)
38. Haocheng Ju and Bin Dong. arXiv:2601.13209, 2026. Ai for mathematics: Progress, challenges, and prospects. arXiv preprint — [arXiv:2601.13209](https://arxiv.org/abs/2601.13209) [find](https://scholar.google.com/scholar?q=Haocheng+Ju+and+Bin+Dong%2E+arXiv%3A2601%2E13209%2C+2026%2E+Ai+for+mathematics%3A+Progress%2C+challenges%2C+and+prospects%2E+arXiv+preprint+%E2%80%94+%5BarXiv%3A2601%2E13209%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2601%2E13209%29)
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](https://api.algebraicgeometry.nl/Article/20170/2024-2-009.pdf). — [doi:10.14231/ag-2024-009](https://doi.org/10.14231/ag-2024-009) [↗](https://api.algebraicgeometry.nl/Article/20170/2024-2-009.pdf)
40. Lean Community. Comparator: A trustworthy judge for lean proof submissions. leanprover/comparator, 2025. GitHub repository. [https://github.com/](https://github.com/) [↗](https://github.com/)
41. Joonkyung Lee and Jaehyeon Seo. Lower bounds for multivariate independence polynomials and their generalisations. arXiv preprint arXiv:2602.02450, 2026. — [arXiv:2602.02450](https://arxiv.org/abs/2602.02450) [find](https://scholar.google.com/scholar?q=Joonkyung+Lee+and+Jaehyeon+Seo%2E+Lower+bounds+for+multivariate+independence+polynomials+and+their+generalisations%2E+arXiv+preprint+arXiv%3A2602%2E02450%2C+2026%2E+%E2%80%94+%5BarXiv%3A2602%2E02450%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2602)
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](https://md.research.elamur.ai/free/en/papers/liu-2026-numina-lean-agent-open-general/). arXiv preprint arXiv:2601.14027, 2026.
43. S Loepp. Constructing local generic formal fibers. Journal of Algebra, 187(1):16–38, 1997. [find](https://scholar.google.com/scholar?q=S+Loepp%2E+Constructing+local+generic+formal+fibers%2E+Journal+of+Algebra%2C+187%281%29%3A16%E2%80%9338%2C+1997%2E)
44. João Lourenço. Grassmanniennes affines tordues sur les entiers. arXiv preprint arXiv:1912.11918, 2019. — [arXiv:1912.11918](https://arxiv.org/abs/1912.11918) [find](https://scholar.google.com/scholar?q=Jo%C3%A3o+Louren%C3%A7o%2E+Grassmanniennes+affines+tordues+sur+les+entiers%2E+arXiv+preprint+arXiv%3A1912%2E11918%2C+2019%2E+%E2%80%94+%5BarXiv%3A1912%2E11918%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1912%2E11918%29)
45. Math, Inc. Completing the formal proof of higher-dimensional sphere packing. sphere-packing, 2026. Blog post. [https://math.inc/](https://math.inc/) [↗](https://math.inc/)
46. Yu Min and Yupeng Wang. Integral p-adic non-abelian hodge theory for small representations. Advances in Mathematics, 458:109950, 2024. [find](https://scholar.google.com/scholar?q=Yu+Min+and+Yupeng+Wang%2E+Integral+p%2Dadic+non%2Dabelian+hodge+theory+for+small+representations%2E+Advances+in+Mathematics%2C+458%3A109950%2C+2024%2E)
47. Mistral AI. Leanstral: Open-source foundation for trustworthy vibe-coding. leanstral, March 2026. Blog post. [https://mistral.ai/news/](https://mistral.ai/news/) [↗](https://mistral.ai/news/)
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. [find](https://scholar.google.com/scholar?q=Masayoshi+Nagata%2E+Local+Rings%2E+Interscience+Tracts+in+Pure+and+Applied+Mathematics%2C+No%2E+13%2E+Interscience+Publishers%2C+a+division+of+John+Wiley+%26+Sons%2C+New+York%E2%80%93London%2C+1962%2E)
49. OpenAI. First Proof? Technical report, OpenAI, February 2026. URL [https://cdn.openai.com/pdf/](https://cdn.openai.com/pdf/) 26177a73-3b75-4828-8c91-e8f1cf27aaa0/oai_first_proof.pdf. OpenAI First Proof submissions. [↗](https://cdn.openai.com/pdf/)
50. Xiangyu Pan and Jiahong Yu. Lift-independence problem in the p-adic simpson correspondence for curves. arXiv preprint arXiv:2605.29947, 2026. — [arXiv:2605.29947](https://arxiv.org/abs/2605.29947) [find](https://scholar.google.com/scholar?q=Xiangyu+Pan+and+Jiahong+Yu%2E+Lift%2Dindependence+problem+in+the+p%2Dadic+simpson+correspondence+for+curves%2E+arXiv+preprint+arXiv%3A2605%2E29947%2C+2026%2E+%E2%80%94+%5BarXiv%3A2605%2E29947%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2605%2E29947%29)
51. Anand Patel. The simplicity of the hodge bundle. arXiv preprint arXiv:2603.19052, 2026. — [arXiv:2603.19052](https://arxiv.org/abs/2603.19052) [find](https://scholar.google.com/scholar?q=Anand+Patel%2E+The+simplicity+of+the+hodge+bundle%2E+arXiv+preprint+arXiv%3A2603%2E19052%2C+2026%2E+%E2%80%94+%5BarXiv%3A2603%2E19052%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2603%2E19052%29)
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. — [doi:10.2140/ant.2021.15.1593](https://doi.org/10.2140/ant.2021.15.1593) [find](https://scholar.google.com/scholar?q=Zev+Rosengarten%2E+Pathological+behavior+of+arithmetic+invariants+of+unipotent+groups%2E+Algebra+%26+Number+Theory%2C+15%287%29%3A1593%E2%80%931626%2C+November+2021%2E+ISSN+1937%2D0652%2E+doi%3A+10%2E2140%2Fant%2E2021%2E15%2E1593%2E+URL+http%3A%2F%2F)
53. Mao Sheng and Yupeng Wang. The small p-adic simpson correspondence in the semi-stable reduction case. arXiv preprint arXiv:2410.09685, 2024. — [arXiv:2410.09685](https://arxiv.org/abs/2410.09685) [find](https://scholar.google.com/scholar?q=Mao+Sheng+and+Yupeng+Wang%2E+The+small+p%2Dadic+simpson+correspondence+in+the+semi%2Dstable+reduction+case%2E+arXiv+preprint+arXiv%3A2410%2E09685%2C+2024%2E+%E2%80%94+%5BarXiv%3A2410%2E09685%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2410%2E09685%29)
54. Qwen Team. QwQ-32B: Embracing the Power of Reinforcement Learning, March 2025. URL [https://qwenlm.github.io/blog/qwq-32b/](https://qwenlm.github.io/blog/qwq-32b/). [↗](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. — [arXiv:2510.04520](https://arxiv.org/abs/2510.04520) [find](https://scholar.google.com/scholar?q=Hanyu+Wang%2C+Ruohan+Xie%2C+Yutong+Wang%2C+Guoxiong+Gao%2C+Xintao+Yu%2C+and+Bin+Dong%2E+Aria%3A+An+agent+for+retrieval+and+iterative+auto%2Dformalization+via+dependency+graph%2E+arXiv+preprint+arXiv%3A2510%2E04520%2C+2025%2E+%E2%80%94)
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](https://md.research.elamur.ai/free/en/papers/yang-2025-qwen3-technical-report/). arXiv preprint arXiv:2505.09388, 2025.

*Updated 3 November 2026*