Proof and certainty · Methods and tools

Can we know a result is true if no human can check every step of its proof?

Some modern proofs depend on computers checking thousands of cases, or run to more pages than any one person could read. This question asks whether knowledge must be something a human mind can survey, or whether trusted machines and communities can know on our behalf.

Claims

A computer follows its instructions exactly and does not tire, so for long case-by-case checks it is more reliable than a person, and a correct program gives knowledge just as a correct proof does.
Mathematicians already rely on results they have not checked themselves; trusting a well-tested program is not very different from trusting a published theorem.

Counterclaims

A proof is meant to explain why a result is true. A computer check can tell us that something is true without giving any insight, which some mathematicians feel is not full mathematical knowledge.
Programs, compilers and hardware can all contain errors, so a computer-assisted proof adds new places where things can go wrong, which human readers cannot easily inspect.

Real-life situations from mathematics

The four colour theorem

In 1976 Kenneth Appel and Wolfgang Haken proved that any map can be coloured with four colours so that neighbouring regions differ, by having a computer check a very large number of configurations. Many mathematicians were uneasy. In 2005 Georges Gonthier and colleagues checked the whole proof with a formal proof assistant, which reassured many of the doubters.

The Kepler conjecture

Thomas Hales announced a proof in 1998 that the familiar greengrocer's stacking of oranges is the densest way to pack equal spheres. The referees reported that they could not be completely certain of every computer step. Hales led a project to verify the proof formally by computer, which was completed in 2014.

Check dates and figures in a reliable source before you use them, and cite that source.

Use this in your TOK work

Essay. Fits titles about technology, trust in experts or whether knowledge needs understanding. Weigh 'knowing that' against 'understanding why'.

Exhibition. A map coloured with four colours, with a note on how the theorem was proved, is an accessible object for a prompt about technology or about the limits of human knowledge.

Link it to the prescribed title or the exhibition prompt you are working on, in your own words. See using maths examples in your essay and choosing exhibition objects.

Themes and study heading

Knowledge and technology Knowledge and the knower Methods and tools

How mathematical knowledge is produced and justified.