![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Mario Carneiro (Chalmers University of Technology)
Tuesday 10 June 2025, 11:45-12:45
Lean Meta-theory: The Proofs behind the Proofs
- đ¤ Speaker: Mario Carneiro (Chalmers University of Technology)
- đ Date & Time: Tuesday 10 June 2025, 11:45 - 12:45
- đ Venue: Seminar Room 1, Newton Institute
Abstract
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 .
Series This talk is part of the Isaac Newton Institute Seminar Series series.
Included in Lists
- All CMS events
- bld31
- dh539
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
Note: Ex-directory lists are not shown.