3 ms·

This makes me wonder if there'll ever be a significant bug discovered in Lean itself, breaking past formalisation work.

by Retr0id 2y ago

pkoird 2y ago
Ahh, so maybe we should first focus on formalizing Lean itself?
- digama0 2y ago
  Should I introduce you to https://arxiv.org/abs/2403.14064 https://arxiv.org/abs/2403.14064 ?
moomin 2y ago
For the problem to affect proofs, it would have to be in the type checker, and the type system isn’t really that complex. The good news is that every single user of Lean checks this works every day. Finding a flaw that literally everyone relies upon and doesn’t notice is pretty implausible.
munchler 2y ago
Lean has a small “kernel” that has been independently checked multiple times, and the rest of Lean depends on the kernel. A soundness bug is still possible, but pretty unlikely at this point. https://lean-lang.org/lean4/doc/faq.html https://lean-lang.org/lean4/doc/faq.html
- norlygfyd 2y ago
  Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.
  - munchler 2y ago
    That would be a bug in math itself, rather than a bug in Lean. It's possible, of course, but even less likely.
deleted 2y ago
[deleted]
digama0 2y ago
Fun fact, there have been 3 soundness bugs in lean 4 so far. (They were all fixed within hours.) I expect we have not yet found them all, but I also do not sleep poorly worried that mathematics will come tumbling down, because these are invariably implementation bugs (either in the literal sense of implementation of the system, or in the implementation of mathematics in the type theory). If something is wrong it is almost certainly going to be the system and not the mathematics. But I'm saying this as someone who works on the proof assistant itself (i.e. hold fixed the mathematics, vary the proof assistant). Kevin Buzzard will say the exact opposite because he is working on the mathematics (vary the mathematics, hold fixed the proof assistant), in which case the likely failure modes will be that a given proof is written poorly, a definition has incorrect behavior on edge cases, etc, but only the current proof is under threat, not some completely unrelated e.g. proof of infinitude of primes deep in the library.

This makes me wonder if there'll ever be a significant bug discovered in Lean itself, breaking past formalisation work.

pkoird 2y ago

Ahh, so maybe we should first focus on formalizing Lean itself?

digama0 2y ago
Should I introduce you to https://arxiv.org/abs/2403.14064 https://arxiv.org/abs/2403.14064 ?

moomin 2y ago

For the problem to affect proofs, it would have to be in the type checker, and the type system isn’t really that complex. The good news is that every single user of Lean checks this works every day. Finding a flaw that literally everyone relies upon and doesn’t notice is pretty implausible.

munchler 2y ago

Lean has a small “kernel” that has been independently checked multiple times, and the rest of Lean depends on the kernel. A soundness bug is still possible, but pretty unlikely at this point. https://lean-lang.org/lean4/doc/faq.html https://lean-lang.org/lean4/doc/faq.html

norlygfyd 2y ago
Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.
- munchler 2y ago
  That would be a bug in math itself, rather than a bug in Lean. It's possible, of course, but even less likely.

deleted 2y ago

[deleted]

digama0 2y ago

Fun fact, there have been 3 soundness bugs in lean 4 so far. (They were all fixed within hours.) I expect we have not yet found them all, but I also do not sleep poorly worried that mathematics will come tumbling down, because these are invariably implementation bugs (either in the literal sense of implementation of the system, or in the implementation of mathematics in the type theory). If something is wrong it is almost certainly going to be the system and not the mathematics. But I'm saying this as someone who works on the proof assistant itself (i.e. hold fixed the mathematics, vary the proof assistant). Kevin Buzzard will say the exact opposite because he is working on the mathematics (vary the mathematics, hold fixed the proof assistant), in which case the likely failure modes will be that a given proof is written poorly, a definition has incorrect behavior on edge cases, etc, but only the current proof is under threat, not some completely unrelated e.g. proof of infinitude of primes deep in the library.