This project presents a discussion of what it means to prove something in mathematics. It outlines the history of proofs and their definitions, as a point of departure, for a case study of whether the proof, of the four colour theorem, by Appel and Haken, is valid and a part of mathematical knowledge. The doubt arises from the fact that the proof, due to being exhaustive with 1476 cases, is assisted by a computer for the critical part of reducing and discharging configurations and is, because of its enormity, uncheckable by human beings. It therefore forms a basis for a controversial subject; do computers deserve a role in pure mathematics? Some of the initial discussion fuelled by the proof is included. To elaborate on this discussion, the project contains the entirely handmade proof of the five colour theorem. These two proofs will form a comparison study of what is lost, on a philosophical level, by having a computer be the formalizer and surveyor. It is concluded that computer-aided proving does not challenge the “infallibility” of mathematical knowledge, but the lack of elegance that this kind of approach is prone to, constitutes a problem for the dissemination within mathematical knowledge.
展开▼
