## Stream: new members

### Topic: Verifying correctness of lean itself

(deleted)

#### Notification Bot (May 06 2022 at 08:29):

A message was moved here from #general > proof automatisation by Eric Wieser.

#### Eric Wieser (May 06 2022 at 08:32):

Hi! It's not a direct answer to your question, but there are third-party tools to check lean proofs such as https://github.com/gebner/trepplein

#### Eric Wieser (May 06 2022 at 08:34):

Arguably what you need to trust is:

• that the proofs that lean can export contain a faithful translation of the original statement (you already have to trust the humans translating math on this)
• The proof checker you use to validate the exported proof (which can either be lean itself, or a third-party tool)

I would guess the paper about Lean itself can give some insight into this design

#### Ratmir Mugattarov (May 06 2022 at 11:12):

I worked a bit with another theorem prover called HOL. They attempted to formally prove correctness of code of HOL with itself.
Is it any interest for similar thing in LEAN?

#### Anne Baanen (May 06 2022 at 11:16):

I believe the correctness proof of HOL was (is?) a huge undertaking. And at the moment Lean is somewhat more popular with mathematicians than computer scientists / logicians, so the interest is probably relatively small.

#### Henrik Böving (May 06 2022 at 11:37):

iirc Leo has mentioned in some talk during the Q&A section that he would welcome if someone would try to do formal verification of the Lean 4 compiler but that it is not of interested to the compiler development team right now and would be a very non trivial undertaking.

Note that, if you tried to verify correctness of the entire Lean 4 compiler right now in Lean you could not actually do this because it uses features like partial that are impossible to analyze with proofs (on purpose).

#### Mario Carneiro (May 06 2022 at 11:56):

#leantt is an (unformalized) proof of consistency of lean's axiomatics

#### Mario Carneiro (May 06 2022 at 11:57):

It would be a feasible but big project to formalize it

#### Mario Carneiro (May 06 2022 at 12:03):

Proving lean's implementation correct is a much bigger project and I don't see it happening in the forseeable future. I've been working on a project along these lines for the past few years (MM0), and a very important part is that it's way simpler than lean, both in theory and in implementation. This is still very uncharted territory, and I would put a bootstrapped verified lean at least 3 years out with a concerted effort by a team of people.

Last updated: Dec 20 2023 at 11:08 UTC