Skip to main content
1 of 4
ntc2
  • 101
  • 5

Look for theorems that have been, or are currently, the subject of major formalization efforts!

The two highest-rated answers as I write this [1,2] -- concerning the Four-Color and Feit-Thompson theorems -- don't mention a major point in the history of those theorems: proofs of both theorems have been completely formalized in the Coq proof assistant in the last ten years: the Four-Color Theorem in 2005 [3] and the Feit-Thompson Theorem in 2012 [4], with both developments led by George Gonthier [7] of Microsoft Research, Cambridge. I believe both of these theorems were chosen for formalization efforts precisely because the existing proofs were so large and complicated that it was considered impossible for a single individual to understand them completely and convincingly.

This is particularly significant for the Four-Color Theorem: while the theorem reducing the problem to finitely many cases was peer reviewed in the original 1976 computer-assisted proof [5], the computer code which checked the finitely many cases in the 1976 proof was not peer reviewed [6] -- indeed the effort to peer review was abandoned after much effort, because the code was judged too long and complex [6]. Contrast this with the 2005 proof: going far beyond peer review, the code has been completely formalized, meaning a specification stating what the code should do has been given -- it should check the finitely many cases correctly -- and they have proven that their code meets that specification. This is an amazing achievement!

The AMS Notices article about the formalization of the Four Color Theorem -- taken from a special issue of the Notices devoted to computer-aided formal proof [9] -- provides a fascinating history of the proof and discussion of the formalization, along with an introduction to computer-aided formal proof for the non-specialist.

The Coq proof assistant [8,10] is a system for constructing and checking completely formal proofs on the computer. Another of it's major success stories is the formalization of an optimizing C compiler [11].

ntc2
  • 101
  • 5