[ajarmst]

The article is interesting, but that lede is incoherent. Many mathematicians accept computer proofs the way chess grand masters accept computer players. Computer “assistants” that generate proofs that humans cannot follow or understand will always be controversial, and the proofs they generate, even though accepted as valid, will always be decorated with an asterisk.

[363849473754]

This is a proof assistant, not an automated theorem prover. The user has to supply* the mathematics and the proof checker formally verifies whether or not the steps are correct. It doesn’t have any creativity (that’s up to the mathematician).

*I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supplied by the user.

[opnitro]

That's not quite true. Many of these proof assistants support some level of automation and proof search. I haven't used Lean specifically, but it's quite common in Coq for projects to write proof search techniques specific to the problem domain and utilize them in their proofs.

[chriswarbo]

True, and Isabelle can call out to automated provers (a mechanism called "sledgehammer"!)

[ajarmst]

Thanks for the clarification.

[6gvONxR4sf7o]

If not an asterisk, they’ll just have less impact. A proof generates a fact. The best facts and proofs are useful in that they help other things. You work becomes useful for my work, which may become useful for others.

[CuriousCosmic]

It's still just as useful. The fact that's proven is what helps other proofs.

A computer assisted proof is just as correct or helpful, it just may be more complicated of a proof initially. Given time said proof can be simplified but having the proof in the first place allows you to move away from assumptions into proofs or alternatively even open new doors that weren't known to exist.

Keep in mind that these computer aided proofs are equivalent to pen and paper proofs but because you can rely on software to guarantee you haven't made any mistakes, you can make more complex proofs that still work.

It's the same as with programming. You can write overly complex and opaque proofs in the same way you can write bad, slow, or hard to read code. It still "works" but it's not ideal and is often a first revision in a series of steps towards the clean, fast, and easy to read final products.

[6gvONxR4sf7o]

The best proofs are good explanations as well as just being correct. If you don’t understand the theorem and the proof as well, you’re less likely to use it.

[kevinbuzzard]

Presumably the asterix denotes "actually true"? ;-)

[LudwigNagasena]

I don’t understand the chess analogy. How is it in any way similar?

[kevinbuzzard]

Lean and the other theorem provers turn mathematical proofs into levels of a computer puzzle game, much like a chess puzzle.