BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.4.0.1//EN
TZID:America/New_York
X-WR-TIMEZONE:America/New_York
BEGIN:VEVENT
UID:955@fds.yale.edu
DTSTART;TZID=America/New_York:20260826T103000
DTEND;TZID=America/New_York:20260826T160000
DTSTAMP:20260817T201155Z
URL:https://fds.yale.edu/events/how-to-generate-and-verify-llm-generated-l
 ean-proofs-for-your-mathematical-needs/
SUMMARY:How to Generate and Verify LLM-Generated Lean Proofs for Your Mathe
 matical Needs
DESCRIPTION:\n\n\nA hands-on workshop on using large language models and Le
 an to formalize mathematical claims\, audit generated proofs\, and determi
 ne whether a machine-verified result actually says what you intended.\n\n\
 n\nWhen Lean says a proof is correct\, what exactly has been proved?\n\n\n
 \nLarge language models can translate mathematical arguments into Lean\, b
 ut a proof that compiles is not necessarily a faithful verification of the
  theorem you intended to state.\n\n\n\nThis workshop introduces a practica
 l workflow for auditing Lean statements and proofs produced by LLMs. Rathe
 r than teaching participants to write Lean proofs from scratch\, we will f
 ocus on the skills needed to evaluate an existing Lean artifact.\n\n\n\nPa
 rticipants will learn how to understand what a formal statement actually s
 ays\, determine whether it matches the original mathematical claim\, and c
 heck whether Lean accepts the proof in a reproducible and trustworthy envi
 ronment.\n\n\n\n\nRegister\n\n
ATTACH;FMTTYPE=image/jpeg:https://fds.yale.edu/wp-content/uploads/2026/08/
 lean-proofs-graphic.png
CATEGORIES:FDS Events,Featured Events,Workshops,Training
LOCATION:Yale Institute for Foundations of Data Science\, Kline Tower 13th 
 Floor\, Room 1327\, New Haven\, CT\, 06511\, United States
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=Kline Tower 13th Floor\, Ro
 om 1327\, New Haven\, CT\, 06511\, United States;X-APPLE-RADIUS=100;X-TITL
 E=Yale Institute for Foundations of Data Science:geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:America/New_York
X-LIC-LOCATION:America/New_York
BEGIN:DAYLIGHT
DTSTART:20260308T030000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR