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.