Mini-Workshop on Human–AI Collaboration in Mathematical Research

Speaker: Jiedong Jiang, Westlake University

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

Time: Wednesday, May 20, 2026, 2:00–3:00 pm

Venue: Room B725, Shuangqing Complex Building

Zoom Meeting ID: TBD

Passcode: YMSC

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 in 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.

Registration:

【腾讯文档】Registration For the Mini-Workshop on Human–AI Collaboration in Mathematical Research

https://docs.qq.com/form/page/DRWJvSmtSb1RiemRw