Zulip Chat Archive

Stream: new members

Topic: Verifying correctness of lean itself

Ratmir Mugattarov (May 06 2022 at 08:27):


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