Events
Featured Events
How to Generate and Verify LLM-Generated Lean Proofs for Your Mathematical Needs
Wednesday, August 26, 2026
10:30AM - 4:00PM
Introduction, demonstrations, and hands-on training
12:00 – 1:00 PM — Lunch (provided)
1:00 – 3:30 PM — Workshop continues
Practical verification, auditing, and common failure modes
3:30 PM — Afternoon tea
Informal conversation following the workshop
A hands-on workshop on using large language models and Lean to formalize mathematical claims, audit generated proofs, and determine whether a machine-verified result actually says what you intended.
When Lean says a proof is correct, what exactly has been proved?
Large language models can translate mathematical arguments into Lean, but a proof that compiles is not necessarily a faithful verification of the theorem you intended to state.
This workshop introduces a practical workflow for auditing Lean statements and proofs produced by LLMs. Rather than teaching participants to write Lean proofs from scratch, we will focus on the skills needed to evaluate an existing Lean artifact.
Participants will learn how to understand what a formal statement actually says, determine whether it matches the original mathematical claim, and check whether Lean accepts the proof in a reproducible and trustworthy environment.
 |
Speaker: Anna Gilbert (Yale) John C. Malone Professor of Statistics & Data Science Yale University |
 |
Speaker: Quanquan Liu (Yale) Assistant Professor, Department of Computer Science Yale University |
Add To: Google Calendar | Outlook | iCal File
- Featured Events
- Workshops
- Training
Submit an Event
Interested in creating your own event, or have an event to share? Please fill the form if you’d like to send us an event you’d like to have added to the calendar.