0

In this question

State of the progess of the automated proof checking

Henning Makholm has answered. I intended to ask about his assertion there as a comment, but since I did not have enough points, I asked it as an answer, which was deleted at the end.

Here I copy my question from there:

  • Could you please give me some references for this assertion "The mechanics of verifying proofs by computer is pretty much a solved problem. We have a good solid understanding of what a valid proof step is and how to recognize its validity by machine."?

A user suggested some wikipedia links as "a good place to start", however, I like a comprehensive reference, instead of only a "good place to start".

For an explicit example: Can the proof of Fermat's last theorem be formalised and then automatically checked?

Note: In your answers, please be to the point: Please provide comprehensive references to Henning Makholm's answer instead of some vague or too general statements.

Tuyen
  • 9
  • I have edited your question to remove irrelevant information taken from that link. – Lee Mosher Jun 20 '19 at 19:57
  • 2
    Given a sequence of statements, and for each statement a pointer to one or two previous statements and the name of a rule of inference (or the name of an axiom), it is really a trivial task to verify that this sequence is a valid proof. - In this extreme, it requires however a lot of work to translate even simple proofs to a verifiable form. But meanwhile systems have become quite good at "guessing" a lot of intermediate steps from a sufficiently good sequence of major steps, so there is less work to translate a proof into something that can be extended to a line-by-line verifiable proof. – Hagen von Eitzen Jun 20 '19 at 20:03
  • Automation and formalization are 2 different things. Automation (usually) refers to the task of creating programs to automatically find proofs. Formalization refers to the task of developing a proof system and transcribing proofs into that system. Although technically it is correct English to say that verifying proofs is automation, it is so trivial that no one uses the terms that way. Usually what you are talking about is described as formalization. – DanielV Jun 20 '19 at 23:46
  • With respect to Fermat's "Last" Theorem, you can only formalize proofs that you understand. And almost no one understands that proof. So probably shouldn't hold your breath on that one. – DanielV Jun 20 '19 at 23:48
  • 1
    The title of this question should be edited to be relevant to the substantive question you're asking. Someone reading the title should have a reasonably good idea of what the question is about. – Derek Elkins left SE Jun 21 '19 at 00:49
  • @Daniel: If I need to understand a proof in order to formalise it, as you wrote, then I wouldn't say "The mechanics of verifying proofs by computer is pretty much a solved problem". Can't every sentence/statement be formalised? – Tuyen Jun 21 '19 at 04:36
  • @Hagen von Eitzen: "In this extreme, it requires however a lot of work to translate even simple proofs to a verifiable form." So this is exactly why I would like Henning Malkholm to provide more details for his assertion. For my explicit question about the proof of Fermat's last theorem, what do you have to say? – Tuyen Jun 21 '19 at 04:41
  • Fermat's Last Theorem seems like a poor choice. Wouldn't your question work just as well for, let's say, the Fundamental Theorem of Calculus? The answer in the linked question, and the comments in this question, all apply equally well to FLT and to the FTC. The difference is that the proof of FTC is much shorter (I teach it in one undergraduate semester, starting from the axioms for the real numbers) and is understood by many, many more people than the proof of the former. So if it hasn't been done for the FTC then it hasn't been done for FLT. But the principles for both are the same. – Lee Mosher Jun 22 '19 at 16:06
  • @LeeMosher: Thank you. I am reading some references about proportional logic, so know a bit about this stuff. Of course, it is nice that FTC can be automatically proof checked. However, it will be nicer if also FLT can be done so. And even more interesting, for claims such as the proof of the ABC conjecture. – Tuyen Jun 22 '19 at 20:58
  • So I would like that, even if one person does not understand much of the proof of some results, but has enough knowledge about fundamental stuffs, he/she can still be able to make a formalised version of that proof, and then check it automatically with some softwares. – Tuyen Jun 22 '19 at 21:00

0 Answers0