Lean4Less: Translating Lean to Smaller Theories via an Extensional-to-Intensional Translation

Add to your list(s) Download to your calendar using vCal

• Rishikesh Vaishnav (ENS Paris-Saclay)
• Thursday 22 January 2026, 17:00-18:00
• Online; live-streamed at MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

Lean is a proof assistant developed by the Lean FRO that has become especially popular with mathematicians in recent years, whose type-theoretic foundations take after the proof assistant Rocq. While Lean’s typechecking kernel attempts to be as minimal as possible, it introduces a number of specialized definitional equalities as conveniences for mathematical formalization. These definitional equalities are crucial to enabling scalable formal developments in Lean, however they complicate metatheoretical analyses and the task of proof export from Lean.

In this talk, I will discuss the theory, design, and implementation of a tool called “Lean4Less” that translates Lean proofs to a smaller theory “Lean-” with fewer such definitional equalities, focusing in particular on the elimination of Lean’s rules of proof irrelevance and “K-like reduction”. Lean4Less implements a special case of a translation from extensional to intensional type theory, inserting explicit type conversions around subterms using generated type equality proofs that are typeable in the Lean- theory. Lean4Less’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.

=== Online talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• Martin's interesting talks
• Online; live-streamed at MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.