Time：15:00-16:30, Thursday, November 6 2025
Venue：E4-233
Speaker: Rongge Xu, Yau Mathematical Sciences Center, Tsinghua University
Biography: Rongge Xu received his Ph.D. in Physics from Westlake University in 2025. She is currently a Postdoctoral Research Fellow at the Yau Mathematical Sciences Center, Tsinghua University. Her research interests lie at the intersection of mathematical physics, category theory, and AI for mathematics.
Title：Lean based AI for Math
Abstract: Modern AI is powerful at pattern discovery yet brittle on reliability, compositionality, and reuse—precisely what mathematics demands. Lean-based AI for Math treats the Lean kernel as a ground-truth arbiter: language models draft steps, retrieval supplies reusable lemmas, and only machine-checked proofs are accepted. We present a practical recipe—minimal SFT to "speak Lean," verifier-in-the-loop reinforcement/repair, and a theorem-graph over mathlib for targeted retrieval and de-duplication—scaling from textbook problems to research-style tasks. We also discuss hybrid pipelines where numerical modules produce error certificates (residual checks) that interface with formal proofs. A demo with LeanBridge, our lightweight multi-agent orchestrator that automates planning, retrieval, error-driven repair, and concise proof explanations, illustrates the end-to-end workflow. The framework aims at transparent, auditable, and shareable mathematical results across different fields.
