4 ms·

What if mathematical theorems are described by executable code instead of just symbols then ? Currently it seems impossible for reader to verify all theorems in

What if mathematical theorems are described by executable code instead of just symbols then ? Currently it seems impossible for reader to verify all theorems in a math paper.

r-zip 5y ago
There are efforts in that direction: https://leanprover.github.io/theorem_proving_in_lean4/ https://leanprover.github.io/theorem_proving_in_lean4/
ABeeSea 5y ago
A major advancement happened this year where a recent paper from a fields medalist on an incredibly abstract topic was formally proved in Lean. The theorem was that Scholze’s new condensed mathematics was logically consistent with real functional analysis. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm...
eigenket 5y ago
Currently transforming a new piece of maths from its "standard" form (i.e. what working mathematicians actually use) to something a computer can understand is a big task that usually takes a team of experts something of the order of years. Maths is really hard and proofs require a tonne of steps. For this reason mathematicians have to be comfortable jumping over the standard pedestrian intermediate steps in proofs and just focusing on the important stuff. This is necessary because including all the details would obscure the important stuff (imagine directions for driving somewhere with steps like "now walk up to the car", "now click the opener", "now open the car door", "now sit down in the drivers seat"). Computers (currently) are way too dumb to skip these steps so you have to walk them through it.
- jkhdigital 5y ago
  And yet… the gold standard for demonstrating that a proof has no “bugs” is to execute it within a proof assistant. The late Fields medalist Vladimir Voevodsky gave a memorable talk on this subject, as part of his motivation for developing Homotopy type theory as a foundational language for mathematics that is very close to the syntax used in proof assistants.
  - jonnybgood 5y ago
    Is it a consensus among mathematicians that is the gold standard? Voevodsky for sure was an advocate but I’m not aware of there being a consensus on the subject.
    - laingc 5y ago
      From my experience as a mathematician, I would say that only a very small minority of mathematicians would accept computer verification of proofs, let alone view it as a gold standard.
  - eigenket 5y ago
    Thats a bit like saying the gold standard for programming is formal verification. Sure in an ideal world maybe every piece of code would be formally verified, but its not realistic and (for the vast majority of use cases) wouldn't be overly useful. A much more realistic "gold standard" for maths is to be peer reviewed and read and understood by a sufficient number of working mathematicians.
joppy 5y ago
This question seems to always come up on Hacker News - figuring out how to even formulate the statement of theorems in theorem provers such as Lean is a massive research undertaking in itself, requiring much creativity and novel work. Let alone figuring out how to formulate the proofs. I’d recommend you have a look at some of the talks that Buzzard has given on this to understand the complications (both technical and social) and progress that has been made so far.
cscurmudgeon 5y ago
See this. It uses first-order logic. http://www.mizar.org/library/ http://www.mizar.org/library/
kovac 5y ago
Logicians study this I think in computability theory. It's a hard problem. https://en.m.wikipedia.org/wiki/Computably_enumerable https://en.m.wikipedia.org/wiki/Computably_enumerable.

What if mathematical theorems are described by executable code instead of just symbols then ? Currently it seems impossible for reader to verify all theorems in a math paper.

r-zip 5y ago

There are efforts in that direction: https://leanprover.github.io/theorem_proving_in_lean4/ https://leanprover.github.io/theorem_proving_in_lean4/

ABeeSea 5y ago

A major advancement happened this year where a recent paper from a fields medalist on an incredibly abstract topic was formally proved in Lean. The theorem was that Scholze’s new condensed mathematics was logically consistent with real functional analysis. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm...

eigenket 5y ago

Currently transforming a new piece of maths from its "standard" form (i.e. what working mathematicians actually use) to something a computer can understand is a big task that usually takes a team of experts something of the order of years. Maths is really hard and proofs require a tonne of steps. For this reason mathematicians have to be comfortable jumping over the standard pedestrian intermediate steps in proofs and just focusing on the important stuff. This is necessary because including all the details would obscure the important stuff (imagine directions for driving somewhere with steps like "now walk up to the car", "now click the opener", "now open the car door", "now sit down in the drivers seat"). Computers (currently) are way too dumb to skip these steps so you have to walk them through it.

jkhdigital 5y ago
And yet… the gold standard for demonstrating that a proof has no “bugs” is to execute it within a proof assistant. The late Fields medalist Vladimir Voevodsky gave a memorable talk on this subject, as part of his motivation for developing Homotopy type theory as a foundational language for mathematics that is very close to the syntax used in proof assistants.
- jonnybgood 5y ago
  Is it a consensus among mathematicians that is the gold standard? Voevodsky for sure was an advocate but I’m not aware of there being a consensus on the subject.
  - laingc 5y ago
    From my experience as a mathematician, I would say that only a very small minority of mathematicians would accept computer verification of proofs, let alone view it as a gold standard.
- eigenket 5y ago
  Thats a bit like saying the gold standard for programming is formal verification. Sure in an ideal world maybe every piece of code would be formally verified, but its not realistic and (for the vast majority of use cases) wouldn't be overly useful. A much more realistic "gold standard" for maths is to be peer reviewed and read and understood by a sufficient number of working mathematicians.

joppy 5y ago

This question seems to always come up on Hacker News - figuring out how to even formulate the statement of theorems in theorem provers such as Lean is a massive research undertaking in itself, requiring much creativity and novel work. Let alone figuring out how to formulate the proofs. I’d recommend you have a look at some of the talks that Buzzard has given on this to understand the complications (both technical and social) and progress that has been made so far.

cscurmudgeon 5y ago

See this. It uses first-order logic. http://www.mizar.org/library/ http://www.mizar.org/library/

kovac 5y ago

Logicians study this I think in computability theory. It's a hard problem. https://en.m.wikipedia.org/wiki/Computably_enumerable https://en.m.wikipedia.org/wiki/Computably_enumerable.