> Firstly, Lean is not as sound as you'd think it is, and long code is just codename for trouble. It is known that Lean has soundness issues in its kernel. There are bugs that allow you to peove, in Lean, that 0=1. Clearly, this is a false statement. But from a false statement (under the theory that runs Lean) we can prove anything else.
I always figured Lean had undiscovered bugs (as does any software), but I didn't realize it had known inconsistencies like this. Anyone curious about why this is a big deal should read up on the Principle of Explosion: https://en.wikipedia.org/wiki/Principle_of_explosion
> Firstly, Lean is not as sound as you'd think it is, and long code is just codename for trouble. It is known that Lean has soundness issues in its kernel. There are bugs that allow you to peove, in Lean, that 0=1. Clearly, this is a false statement. But from a false statement (under the theory that runs Lean) we can prove anything else.
I always figured Lean had undiscovered bugs (as does any software), but I didn't realize it had known inconsistencies like this. Anyone curious about why this is a big deal should read up on the Principle of Explosion: https://en.wikipedia.org/wiki/Principle_of_explosion