BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Lean4Less: Translating Lean to Smaller Theories via an Extensional
 -to-Intensional Translation - Rishikesh Vaishnav (ENS Paris-Saclay)
DTSTART:20260122T170000Z
DTEND:20260122T180000Z
UID:TALK243022@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:Lean is a proof assistant developed by the Lean FRO that has b
 ecome especially popular with mathematicians in recent years\, whose type-
 theoretic foundations take after the proof assistant Rocq. While Lean's ty
 pechecking kernel attempts to be as minimal as possible\, it introduces a 
 number of specialized definitional equalities as conveniences for mathemat
 ical formalization. These definitional equalities are crucial to enabling 
 scalable formal developments in Lean\, however they complicate metatheoret
 ical analyses and the task of proof export from Lean.\n\nIn this talk\, I 
 will discuss the theory\, design\, and implementation of a tool called "Le
 an4Less" that translates Lean proofs to a smaller theory "Lean-" with fewe
 r such definitional equalities\, focusing in particular on the elimination
  of Lean's rules of proof irrelevance and "K-like reduction". Lean4Less im
 plements a special case of a translation from extensional to intensional t
 ype theory\, inserting explicit type conversions around subterms using gen
 erated type equality proofs that are typeable in the Lean- theory. Lean4Le
 ss's implementation is based on a modification of a typechecker kernel for
  Lean taken from the "Lean4Lean" project\, and effects our translation by 
 generating translated terms in parallel to normal typechecking.\n\n\n=== O
 nline talk ===\n\nJoin Zoom Meeting https://cam-ac-uk.zoom.us/j/8985609195
 4?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1\n\nMeeting ID: 898 5609 1954 Passco
 de: ITPtalk
LOCATION:Online\; live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR