Yale Institute for Foundations of Data Science

How to Generate and Verify LLM-Generated Lean Proofs for Your Mathematical Needs

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.

No Lean experience required No programming required Hands-on training

August

26
2026
10:30 AM – 3:30 PM Wednesday, August 26
Kline Tower · Room 1327 219 Prospect Street
Yale University
Lunch included 12:00 – 1:00 PM
Afternoon tea Beginning at 3:30 PM
Hosted by: Yale FDS
Organizers: Anna Gilbert & Quanquan Liu
Location: Kline Tower, Room 1327
Registration: $1
About the workshop

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.

Designed for beginners

No prior knowledge is required. You do not need experience with Lean, proof assistants, formal methods, programming, Visual Studio Code, or command-line tools.

A practical verification workflow

From mathematical idea to verified artifact.

1

Generate

Use an LLM to translate a mathematical statement or argument into Lean.

2

Inspect

Identify assumptions, quantifiers, mathematical domains, conclusions, and the structure of the proof.

3

Verify

Confirm that Lean accepts the proof in a reproducible environment without incomplete proofs or unacceptable trust dependencies.

4

Audit

Determine whether the formal theorem Lean verified is genuinely the theorem you meant to prove.

What you'll learn

Read Lean critically, without becoming a Lean programmer.

Read the formal statement

Locate and interpret the theorem's assumptions, conclusion, quantifiers, variables, mathematical domains, and proof body.

Compare formal and informal claims

Determine whether the Lean statement faithfully represents the mathematical theorem or natural-language argument you started with.

Recognize subtle failure modes

Spot weakened conclusions, changed quantifier order, vacuous assumptions, altered domains, and other ways a formally correct proof can verify the wrong theorem.

Check the proof itself

Learn how to confirm that a proof compiles reproducibly and does not rely on incomplete proofs or unacceptable trust dependencies.

Who should attend

For anyone who wants to use Lean as a verification tool.

This workshop is intended for researchers, mathematicians, scientists, students, and others interested in using LLM-generated Lean output to check their own mathematical statements and natural-language proofs.

The emphasis is not on becoming a formal-methods expert. It is on developing enough fluency to ask the right questions of an LLM-generated proof and decide whether the result can actually be trusted.

Also during the workshop

Participants will learn about opportunities to serve as evaluators for a project on Lean-verified counterexamples.

Registration

A little skin in the game.

Registration costs just $1. We simply ask that if your plans change, you let us know in time to offer your place to someone else.

Cancel by Sunday, August 23 and your $1 registration fee will be refunded.

If you register, do not cancel by the deadline, and do not attend the workshop, you will be charged a $100 no-show fee.

In other words: come to the workshop, or cancel on time. That's it.

$1 to register
✓
Attend You're all set.
✓
Cancel by August 23 Your $1 registration fee will be refunded.
!
No-show without timely cancellation $100 no-show fee.
Schedule

Wednesday, August 26

10:30 AM
Workshop begins
Introduction, demonstrations, and hands-on training
12:00 – 1:00 PM
Lunch
Lunch will be 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
Organizers & Host

Workshop leadership

Anna Gilbert
Workshop Organizer
Quanquan Liu
Workshop Organizer
Emily Hau
Associate Director, Yale FDS
Location

Yale University

Kline Tower

Room 1327

219 Prospect Street
New Haven, Connecticut

The workshop will take place on the 13th floor of Kline Tower.

Ready to put an LLM-generated proof to the test?

Join us at Yale for a practical introduction to generating, reading, auditing, and verifying Lean proofs — no Lean or programming experience required.

Register for $1
Wednesday, August 26 · Kline Tower, Room 1327