University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > The Lean Theorem Prover

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

The Lean Theorem Prover

Download to your calendar using vCal

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

BPR - Big proof

Lean is a new, open source, interactive theorem prover designed to
support mathematical reasoning as well as hardware and software
verification. Because its logical foundation, dependent
type theory, has a computational interpretation, we can use Lean
as a programming language and evaluate expressions with a fast
bytecode evaluator. We obtain a metaprogramming language—
that is, a language that we can use to construct expressions
and proofs in dependent type theory itself—by exposing Lean
internals through a suitable API . This provides us with a means
of extending Lean's functionality and automation within Lean
itself. In this talk, I will describe this
metaprogramming framework and some of its mechanisms for manipulating
expressions efficiently.

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

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Horizon Seminars in person & via zoom Average on Saturdays: 7535.16981132 kWh

Other talks

Title to be confirmed The United States of America at 250: Reflections on the Past, Present and Future of Independence Necessary mechanisms for super AI and stopping hallucinations: The consistent reasoning paradox and the indeterminacy function Title to be confirmed Title to be confirmed Discovery Investigations: Science, Empire and the Making of the British South Atlantic
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity