Hacker News Reader

Comment by revskill | Hacker News Reader

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.

View on HN

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.

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.

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.

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.

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.

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-confirm...

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

Logicians study this I think in computability theory. It's a hard problem.

https://en.m.wikipedia.org/wiki/Computably_enumerable.

See this. It uses first-order logic.

http://www.mizar.org/library/

Reply on news.ycombinator.com