The Greek concept of apodictic proof, as exemplified by geometrical demonstration in Euclid’s Elements, and refined during the 17th-18th centuries in the form of analytic proof, became the major characteristic of the European mainstream mathematical culture. Gödel’s investigations in meta-mathematics, after the 20th-century foundational crisis, shook down the established belief in the identification of truth with proof. During the subsequent years, mathematical logicians developed powerful methods for the formal representation of proofs in different formal languages. Nevertheless, many mathematicians were not willing to accept the new ideal of formalistic proof. Mac Lane, for instance, emphasized that
Real proof is not simply a formalized document, but a sequence of ideas and insights. [Mac Lane 1997, 152]
The appearance of computer-generated proofs in 1976, by Kenneth Ira Appel (1932-) and Wolfgang Haken (1928-) for the solution of the famous four-color problem, and t...