We Need a Better Style of Proof
William M. Farmer
2016
Abstract
Proofs serve several diverse purposes in mathematics. They are used
to communicate mathematical ideas, certify that mathematical results
are correct, discover new mathematical facts, learn mathematics,
establish the interconnections between mathematical ideas, show the
universality of mathematical results, and create mathematical beauty.
Traditional proofs and (computer-supported) formal proofs do not
fulfill these purposes equally well. In fact, traditional proofs
serve some purposes much better than formal proofs, and vice versa.
For example, traditional proofs are usually better for communication,
while formal proofs are usually better for certification. We will
compare both traditional and formal proofs with respect to these seven
purposes and show that both styles of proof have serious shortcomings.
We will offer a new style of proof in which (1) informal and formal
proof components are combined (in accordance with Michael Kohlhase's
notion of flexiformality), (2) results are proved at the optimal level
of abstraction (in accordance with the little theories method), and
(3) cross-checks are employed systematically. We will argue that this
style of proof fulfills the purposes of mathematical proofs much
better than both traditional and formal proofs.