Verifying correctness of lean itself

Stream: new members

[Ratmir Mugattarov]

(deleted)

[Notification Bot]

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

[Eric Wieser]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

It would be a feasible but big project to formalize it

[Mario Carneiro]

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.