[edgyquant]

I’ve long awaited the day we have automated proof checking. As someone who started in CS but went for a degree in Mathematics I held on to the idea of some sort of test suite that newer mathematicians (who have tend to come up with already existing or already disproven proofs for fun while thinking they’re on to something) could run to determine if they’re wasting their time and it not have to be a class mate making fun of them (sadly I’ve done this to kids who were just excited to try and learn, as if I had any room to talk.)

And it would only scale from there, hell we could run such a test suite against all known proofs and who knows how many ancient theorems we could disprove. I don’t think this is the test suite but something like it and the ANN that OpenAI build to check proofs is a good start.

[ezequiel-garzon]

What do you gain from automated proofs? Take the infinitude of primes. Plenty of textbooks different proofs of this fact to deepen your insight. Having an oracle-like entity tell me whether something is true or false is unlikely to have the same result, and I’m afraid “following the automated proof” won’t help much in this regard.

[drdeca]

They aren't talking about something that tells you whether a statement is true or false, but something which you can present your line of reasoning to, and it will check that your reasoning doesn't include an invalid step, or a gap that would need to be filled in.

I've definitely had the experience of "I think this is a valid proof. I haven't seen it presented anywhere else, and I'm not super familiar with the subject matter. It feels a little socially awkward to ask someone to check if it is right", and I started trying to express it in Lean.

However, I found it difficult to get the implicit type parameters to work right, so I had trouble even formulating the claim in Lean. (the claim was a claim in category theory, and the category theory library for Lean has lots of implicit argument stuff, and probably shouldn't have been the first thing I tried to use Lean for. Also the claim I was trying to show is probably very simple for category theory people.)

[dddbbb]

Increased assurance that the proof is correct and the various standard benefits of digital over analogue data. This software automatically checks the validity of the proof (with a very small, manually verified core of code doing so), it does not automatically generate proofs wholesale. The proof itself is written by the mathematician interactively, which is still a manual process that requires skill, creativity and thought.

[mturmon]

One of the usual examples given in reaction to this question is the puzzle of Euclid's 5th postulate, the parallel-lines postulate. People tried for centuries to prove that it could be deduced from the other axioms. Turned out, it was independent of the others.

A proof system could identify cases where you need hidden assumptions in order to make proofs. In this case, you would get a null result from the oracle, which would be valuable in itself.

[1] https://en.wikipedia.org/wiki/Parallel_postulate

[roywiggins]

At best an proof-checker can invalidate a purported proof, it absolutely is not going to prove that no proofs are valid (it would have to affirmatively prove that the result is actually independent of the axioms you picked, which is a lot harder)

[mturmon]

Many incorrect proofs of this postulate were given over the years. (For instance, in some cases these erroneous proofs have steps that implicitly use the postulate itself.)

The proof checker could detect such errors in a purportedly clean proof.

[bolus]

First of all, mathematics is not about T/F. Think of the axiom of choice, the law of excluded middle, the axiom of inaccessible cardinals, etc.

For the second, understanding why and actually proving something can be related but they're not equivalent. Of course, the intuitive ideas can lead to the right formal technicalities but it is not always the case.

There are two aspects of mathematical proofs-communication of ideas and formal verification. Confusing these distinction can be dangerous and this is why mathematicians led to the area of type theory and formal proofs.

Voedovsky, you can google him to find who he was, lost his faith in "human proof checking" after some error on his peer-reviewed and published result was accidentally discovered after years of nobody doubting its validity.

He dreamed of the world where people do and enjoy mathematics freely leaving the boring parts to computers like mathematicians in nowadays don't worry about how their writing will be published and communicated. What we do is write a proof and leave actual typesetting to the computer. It's called (La)TeX.

What you're saying is like claiming this program is correct because its logic is correct without ever knowing whether the code itself would get compiled or not. More extremely, there's no value for having more and more pseudocodes that we don't know they'll ever terminate or not.

[Koshkin]

> automated proofs

You've got a point, but in this case you are barking at the wrong tree. Aren't they talking about automated proof-checking?

[Smaug123]

Yes, though waves hands machine learning can in principle be used to create a proof-generator from a proof-checker.

[Strilanc]

You could ask questions that would normally take hours or days or years to know the answer to, and have the answer immediately. Sure you still need to work on understanding why, but you'd only work on understanding why for something correct. How could that not lead to a stronger intuition?

[edgyquant]

It’s more something that can tell you if you’ve already been disproven and it would save man hours.