4 ms·

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

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.

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.