Speaker: Dr. Jiedong Jiang ，Westlake University

Title: End-to-End Automated Conjecture Resolution with Formal Verification

Language: Chinese

Time & Venue: 2026.05.13 10:30-11:30 MCM110

Abstract: Can large language models reliably solve research-level open problems and produce verifiable proofs? In this talk, I present a framework that integrates an informal reasoning agent, Rethlas, with a formal verification agent, Archon, to achieve fully automated end-to-end conjecture resolution. Rethlas explores solution strategies by combining reasoning primitives with a semantic theorem search engine, while Archon translates the resulting arguments into fully verified Lean 4 proofs through structured decomposition and iterative refinement. Using this framework, we automatically resolve an open problem in commutative algebra posed by D. D. Anderson (2014) and formally verify the proof in Lean 4. I will discuss how theorem retrieval enables the discovery of critical cross-domain techniques, how the formal agent autonomously fills nontrivial gaps in informal arguments, and the broader implications for human–AI collaborative mathematical research.