Answer by mathy for Why is it so difficult to write complete (computer verifiable) proofs?

2010-05-11T19:53:30Z

There was a special issue of AMS Notices on formal proof in 2008, which discusses some of the difficulties with formal proofs in passing. Freek Wiedijk (who wrote one of the Notices articles) has plenty of good resources on his home page.

In general, one shouldn't underestimate pragmatic difficulties with the current technology of proof assistants, especially with respect to usability. As of today, formal proofs look more like computer code than actual mathematics.

What makes this issue even worse is that many proof assistants in common use are "procedural" proof assistants. A proof in a procedural proof assistant is a linear list of proof "tactics" which manipulate the proof state directly, with no express reference to intermediate goals or hypotheses. These linear scripts are unreadable unless replayed step-by-step in the proof assistant. (They're also extremely brittle, since a slight improvement in the proof tactics themselves can change the expected proof state and make the proof script almost useless.)

More modern proof assistants use declarative proof style, which does not have these problems and reads more like an informal proof.

Of course, one other issue is that each proof assistant brings its own logical foundations, syntax and special tactics: results are generally unportable between different systems, and each system may be more tailored to some branches of mathematics than others.

On the upside, proof formalization can be playful and even addictive: the ability to "interact" with the proof state and get immediate confirmation of successful steps makes for an engaging activity akin to solving a puzzle.

User mathy - MathOverflow

Answer by mathy for Why is it so difficult to write complete (computer verifiable) proofs?