Lean Meta-theory: The Proofs behind the Proofs

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

• Mario Carneiro (Chalmers University of Technology)
• Tuesday 10 June 2025, 11:45-12:45
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

BPRW03 - Big proof: formalizing mathematics at scale

Lean is a theorem prover, but the theory behind the proof system that is implemented is not well understood (by either the users of the system or by type theory researchers). In this talk, I will present some recent work on the type theory of lean, and a progress report on the Lean4Lean project which endeavors to verify a practical lean kernel. I will also present some novel discoveries regarding the axiomatic strength of Lean’s inductive mechanism, a cornerstone of the theory, and their implications for the development of a tool to automatically check whether proofs in Lean can be replayed to work in ZFC .

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.