3 ms·

I think their point is it’s turtles all the way down. At some point you’re relying on software, kernel or otherwise, which will always have the possibility for

I think their point is it’s turtles all the way down. At some point you’re relying on software, kernel or otherwise, which will always have the possibility for bugs. It seems like Lean is an interesting tool that maybe could help with proving, but ultimately will never be authoritative itself as a statement of proof. Of course, this is ultimately a philosophical debate, which hinges on the fact to at while Lean may be demonstrably correct in any number of known applications, there are no guarantees that it is and will remain correct. Such is the nature of software.

enricozb 2y ago
Such is the nature of math as well.
- appplication 2y ago
  I’m not a mathematician, so I’d be interested in any perspectives if the two are ultimately so similar in this regard, or is there is something foundationally different about the traditional mathematical approach. I suppose any proof is ultimately a matter of review and consensus, and potentially would rely on some fundamentally unprovable assumptions at a basic level (e.g. the underlying laws of the universe).
  - golol 2y ago
    It is a fundamentally different manner. Proofs in Lean are formal all the way down. The kernel checks the validity of a proof. This is a finite program checking the validity of the kernel to high degree once is different to checking the validity of every new paper that comes out to high degree.
    - ChadNauseam 2y ago
      Yes, the human effort of checking proofs written in Lean is O(1) as you only need to verify the kernel. The human effort of checking proofs written traditionally is O(N). Of course writing proofs in Lean is much more difficult (for now) and, checking the proof is not the only interesting part. Other mathematicians also want to understand the proof, and this will always be O(n). Also, while it's true that bugs in mathlib cannot cause lean to accept invalid proofs as long as the kernel is correct, bugs in mathlib can still be annoying (I have only used lean briefly and I got stuck for a long time on a buggy tactic that was silently messing up my proof state).
      - golol 2y ago
        My personal belief is that translating an informal proof from a paper to a proof in Lean, given that the prerequisites are already formalized, is an O(n) operation where n is the length of the proof. It's just translation. Right now the constant is something like 10-100, but I think with more work on matlib and AI assistance it can be brought down to maybe 1-3, meaning formalising proofs right as you write them becomes feasible. In fact the constant may go below 1 as formalization in Lean can prevent unseen errors from slowing your progress.
  - enricozb 2y ago
    What I was referring to is that we don't know if ZFC, for example, is consistent. And it is only consistent if there are unprovable statements. And of course, you can't know which statements are unprovable (because then you would prove its consistency). So, in some sense you're always chasing your own tail. Theorems might be proven true only because ZFC is inconsistent and therefore everything can be proven. The Lean language is known to be equivalent to ZFC + {existence of n < omega inaccessible cardinals}, which is roughly the common language of mathematics. The actual implementation of the kernel _may_ have bugs, but that's sort of separate from the language definition. The sentiment I see for the purpose of Lean now and in the near future is for more collaborative mathematics. Theorems and structures are more transparent and concrete (the code is right there). Results are more consumable. The community does not seem to see its main purpose being a way to quell doubts of a paper proof.
konstantinua00 2y ago
I think the counterpoint is it's turtles all the way down. At some point you're relying on human mind, logic or otherwise, which will always have possibility of misunderstandings and mistakes. It seems like Mahematicians are interesring tools that maybe could help with proving, but ultimately will never be authorative itsel as a statement of proof. Of course, this is ultimately a philosophical devate, which hinges on the fact to at while Mathematicians may be demonstrably correct in any number of known applications, there are no guarantees that they are and will remain correct. Such is the nature of wetware. --- development of proof assistants is in noticable part fueled by the same fear - fear that wetware had a fault somewhere in the long ladder of math, causing all the layers above be a useless junk and those things did happen, it isn't just an imagined threat what proof assistants propose is a clever trick - write one, simple, kernel. Stare at those 100 lines of code. Stare at mathematical definitions of intended API. Conclude that those coincide. Then use that kernel on the text files with all the proof ladder All mistrust of "whole mathematics" gets condensed in mistrust of 100 lines of code And mistrust of wetware gets replaced with mistrust of hardware - something we already do since even before computers appeared

enricozb 2y ago

Such is the nature of math as well.

appplication 2y ago
I’m not a mathematician, so I’d be interested in any perspectives if the two are ultimately so similar in this regard, or is there is something foundationally different about the traditional mathematical approach. I suppose any proof is ultimately a matter of review and consensus, and potentially would rely on some fundamentally unprovable assumptions at a basic level (e.g. the underlying laws of the universe).
- golol 2y ago
  It is a fundamentally different manner. Proofs in Lean are formal all the way down. The kernel checks the validity of a proof. This is a finite program checking the validity of the kernel to high degree once is different to checking the validity of every new paper that comes out to high degree.
  - ChadNauseam 2y ago
    Yes, the human effort of checking proofs written in Lean is O(1) as you only need to verify the kernel. The human effort of checking proofs written traditionally is O(N). Of course writing proofs in Lean is much more difficult (for now) and, checking the proof is not the only interesting part. Other mathematicians also want to understand the proof, and this will always be O(n). Also, while it's true that bugs in mathlib cannot cause lean to accept invalid proofs as long as the kernel is correct, bugs in mathlib can still be annoying (I have only used lean briefly and I got stuck for a long time on a buggy tactic that was silently messing up my proof state).
    - golol 2y ago
      My personal belief is that translating an informal proof from a paper to a proof in Lean, given that the prerequisites are already formalized, is an O(n) operation where n is the length of the proof. It's just translation. Right now the constant is something like 10-100, but I think with more work on matlib and AI assistance it can be brought down to maybe 1-3, meaning formalising proofs right as you write them becomes feasible. In fact the constant may go below 1 as formalization in Lean can prevent unseen errors from slowing your progress.
- enricozb 2y ago
  What I was referring to is that we don't know if ZFC, for example, is consistent. And it is only consistent if there are unprovable statements. And of course, you can't know which statements are unprovable (because then you would prove its consistency). So, in some sense you're always chasing your own tail. Theorems might be proven true only because ZFC is inconsistent and therefore everything can be proven. The Lean language is known to be equivalent to ZFC + {existence of n < omega inaccessible cardinals}, which is roughly the common language of mathematics. The actual implementation of the kernel _may_ have bugs, but that's sort of separate from the language definition. The sentiment I see for the purpose of Lean now and in the near future is for more collaborative mathematics. Theorems and structures are more transparent and concrete (the code is right there). Results are more consumable. The community does not seem to see its main purpose being a way to quell doubts of a paper proof.

konstantinua00 2y ago

I think the counterpoint is it's turtles all the way down. At some point you're relying on human mind, logic or otherwise, which will always have possibility of misunderstandings and mistakes. It seems like Mahematicians are interesring tools that maybe could help with proving, but ultimately will never be authorative itsel as a statement of proof. Of course, this is ultimately a philosophical devate, which hinges on the fact to at while Mathematicians may be demonstrably correct in any number of known applications, there are no guarantees that they are and will remain correct. Such is the nature of wetware. --- development of proof assistants is in noticable part fueled by the same fear - fear that wetware had a fault somewhere in the long ladder of math, causing all the layers above be a useless junk and those things did happen, it isn't just an imagined threat what proof assistants propose is a clever trick - write one, simple, kernel. Stare at those 100 lines of code. Stare at mathematical definitions of intended API. Conclude that those coincide. Then use that kernel on the text files with all the proof ladder All mistrust of "whole mathematics" gets condensed in mistrust of 100 lines of code And mistrust of wetware gets replaced with mistrust of hardware - something we already do since even before computers appeared