Hacker News Reader

The tools are not ready. Using proof assistants isn't possible in many areas of maths as the foundational concepts have not yet been built up from fundamental primitives. Even when it is possible, using proof assistants takes far more work, and the proofs are much more verbose and hard for humans to understand. The tools will be ready when the concepts are available for any subfield, when the results are easy to read, and when it takes a reasonable amount of work (ideally it will be faster than doing it by hand).

I agree the tools are not ready because, as you say, the foundational concepts are not yet encoded.

But for OP, the point isn't having humans understand. It's having the computer check the proof. You still use traditional journal papers for communicating the proof to humans. You're just also able to say "The proof has been verified and really is true."

Yes, but humans using the proof assistants need to be able to read and understand the proofs while they are constructing them.

ideally it will be faster than doing it by hand

That's a good point... I agree the tools are not ready. Most computer-assisted tools make it easier to do your work. It's easier to type a five page paper in Word than it is to write it longhand. But for now it's a lot more work to encode a proof in a proof assistant than to just write it up in LaTeX (which I think a lot of people don't realize).

It's not just that the foundational concepts are missing, it's also that proof assistants currently require you to fill in much more detail than human proofs do. You can't just write something like... "this corollary is trivial", or, "since x is a power of 10, obviously cos(x^2) is irrational"; you have to spell out a proof.

Is there a proof here at all? The only thing mentioned in the article is a computation.

With due respect, computer-readable proofs are not very interesting to me as a mathematician. I don't see why we should do it. Reproducibility is not a concern.

I have trouble imagining a mathematician wouldn’t welcome formal verification of eg. the classification of finite simple groups.

Most mathematicians don't care about being exactly right. They only need to not see a contradiction. Since most pure math is not used for anything except more math, mistakes rarely have consequences.

A computer is only a threat, that might find a mistake that humans miss.

This (ahem) contradicts my experience. Most mathematicians I’ve met are excited about formal verification, especially the recent progress toward CFT.

Thompson himself has said he’d like his contributions to the classification of finite simple groups verified in his lifetime, and actively followed/encouraged the Coq implementation of his odd order theorem back in 2012.

> recent progress toward CFT

What's this?

Buzzard's group at ICL, eg. Ashvni Narayanan.

Some steps of the proof are left out. In particular, the correctness of the computation for its purpose is omitted :)

>The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness.

What if the algorithms have errors? What if a cosmic ray flips one bit of memory?

100% accuracy will never be achievable. What might be achievable, though, is a higher degree of confidence than we currently have. Of course, the correctness of algorithms should also have to have a computer validated proof.

> What if the algorithms have errors?

Errors will always happen.

> What if a cosmic ray flips one bit of memory?

Run it several times and compare results until you reach the desired level of statistical certainty.

>The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness.

This seems like a strong overstatement. We got by for more than 2000 years without computer-readable proofs, relying on intuition and validation.

With lots of major mistakes along the way.

As another example of this, In [1] I've taken a python program for counting (a bound on) the number of iterations needed of the SafeGCD algorithm to compute a modular inverse for any 256-bit (relatively prime) modulus, translated the python into Coq, and proved the implementation correct. Then by running the computation within Coq we produce a theorem about the bounds (e.g. at most 590 iterations needed for the HD variant of the algorithm).

[1] https://blog.blockstream.com/a-formal-proof-of-safegcd-bound...

> The tools are ready, it is just that doing the hard work going from a handwritten one to a computer-readable proof is not sufficiently appreciated.

Seems like a perfect task for an LLM trained on English and Idris/Coq/etc

> As this incident demonstrates, errors can easily creep into mathematical proofs, even those written by experts. The only way to mitigate this is to use computer-readable proofs, (...)

Ironically, computer programs seem to be a lot more error prone than mathematical proofs. Yes, errors in mathematical proofs happen, but they're rare enough that the they're widely reported in the (mathematical) community. Errors in computer programs on the other hand are a virtual guarantee.

Ironically, emails and essays seem to be out more error prone than mathematical proofs...

1. Proofs are intended to be correct. The vast majority of computer programs are intended to be practical, and are far far larger than the largest math proofs. Where correctness matters, computer programs have fewer bugs.

2. Nearly every non-computerized mathematical proof is not even a proof, it is a sketch that requires a lot of hand waving and logical jumps to be interpreted. Likewise, specs have fewer bugs than concrete program, because they aren't complete.

A math professors blew my mind once by telling me that a paper full of errors was still good work and could be salvaged. He went on to say that most good work was like that. In the worst case you end up proving something else, but typically you can prove what you initially set out for. I found that so strange I had to confirm it with another, who concurred.

The reason for this is that mathematical papers are fundamentally about an insight about mathematical objects. The insight typically comes from the mathematician having a deep understanding of the mathematical objects. The theorems are some formalised statement that should be true based on the deep understanding. The proofs are something else entirely, a sequence of steps which combine to verify the theorem but where many steps may result from trial-and-error searching for a path forward. Coming from a good mathemematician, the original insights are much more likely to be correct than the details of the proof steps.

> but they're rare enough that the they're widely reported in the (mathematical) community.

You should ask math professors how often there are errors in papers. Every one has their own ratio, but I've heard numbers as high as 30%. However, the general belief is the results are still correct, so few are worried about building with a pile of cards.

See https://academia.stackexchange.com/questions/143374/extent-o...

A computerised proof checker is much less likely to have a mistake than a typical computer program - or a mathematical proof - because it's extremely simple.