5 ms·
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 g
by 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 agoIs 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 agoFrom 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 agoThats 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.