Hacker News Reader

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.

View on HN

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.

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.

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.

Reply on news.ycombinator.com