2
$\begingroup$

Does there exist a mathematical text that references a formal computer verified proof for every theorem it presents? I'm imagining a digital textbook that gives the higher level concepts in typical prose but also provides a means to examine each logical step in as much detail as desired. If not, is such a thing feasible or likely to be attempted?

$\endgroup$
3
  • 5
    $\begingroup$ I imagine the answer is "no", as the level of detail of a computer-verified proof would have little to no practical value to a reader, and would likely be much harder to get through than a normal textbook. That being said, isa-afp.org is a database of computer-verified proofs that may be useful. $\endgroup$
    – NMister
    Jul 17, 2018 at 3:10
  • $\begingroup$ @NMister I was kind of imagining something where the prose follows the formal proof at a high level and provides links to increasing detail that the reader can follow if a certain step needs clarification. They wouldn't have to read it at the finest detail, but it would be easily accessible if needed. $\endgroup$
    – user695931
    Jul 17, 2018 at 3:19
  • 1
    $\begingroup$ The demand for formality strikes me as perhaps a more severe restriction than you would envision, but the book that comes to my mind is Homotopy Type Theory -- Univalent Foundations for Mathematics. It is available in printed form and in PDF downloads. $\endgroup$
    – hardmath
    Jul 17, 2018 at 3:35

1 Answer 1

3
$\begingroup$

Not a textbook but a blog article by Timothy Gowers discussing the ability for computers to write proofs to problems at the level of analysis 1. Here he says

"a few years ago I teamed up with a colleague of mine, Mohan Ganesalingam, to write a computer program to solve easy problems."
and then he goes on to discuss the process

Here's the link https://gowers.wordpress.com/2014/02/03/how-to-work-out-proofs-in-analysis-i/

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .