1 Mechanising thought
The human craving for certain knowledge goes back a long way. There are records, from as far back as ancient Greece, of the thirst for knowledge that provides a fixed anchor for our thinking and can’t be unsettled by new information or doubt. Ever since the time of Euclid (300 BC), mathematical practice has been a role model for establishing such knowledge.
In his Elements, a series of 13 books, Euclid put geometry on an apparently firm footing by showing how mathematical claims about figures (triangles, squares and so on) can be established beyond doubt (Figure 2). The idea is to give a proof.
A proof starts from several axioms, that is, simple claims that are beyond dispute. The proof shows how to arrive at new claims by combining the information from the axioms. Each step in a proof follows a recipe that is guaranteed to produce new true claims from already known true claims. In short, Euclid showed us a method for producing certain knowledge.
When one mathematician (A) wants to convince another (B) of a claim, this method guarantees success (at least in theory). A produces a proof which shows that the claim follows from the axioms. There is no scope for disagreement. If the steps in the proof lead from the axioms to the claim, the claim must be accepted by B.