Formal Verification in Lean
A tutorial on machine-verified proofs
Event Details
Date
Friday, September 4, 2026
Time
10-11:30 a.m.
Location
Description
This tutorial introduces the Lean interactive theorem prover, a programming language for writing mathematical definitions, theorems, and machine-checked proofs. Lean has recently become infrastructure for AI: Google DeepMind, OpenAI, and Anthropic all announced research-level mathematical results whose proofs were formalized as Lean code. After a live introduction to writing lean proofs, participants will get hands-on experience formalizing results from mathematics and computer science.
Cost
Free
Contact
Accessibility
We value inclusion and access for all participants and are pleased to provide reasonable accommodations for this event. Please call 718-902-5854 or email sjain298@wisc.edu to make a disability-related accommodation request. Reasonable effort will be made to support your request.