Concept

Computer-assisted proof

A proof in which some steps are computations too long to check by hand, carried out by a program. It is as rigorous as the program is correct, which is why such proofs are written to be rerun independently and checked with exact or interval arithmetic.

Named by 4 essays across 3 fields — each of them below, with the objects they name alongside it.

A wheel of 5 rim regions needs 4 colours. A hub touching 5 rim regions arranged in a ring. The rim is odd, so the whole map needs 4 colours and no fewer.

Four colours, and a proof nobody can read

Every map on a plane can be coloured with four colours so that no two neighbours match. The statement is understandable by a child, it resisted a century of attempts, and the proof that settled it cannot be checked by a human being.

discrete · Graph colouring
A quadrilateral the Hénon map carries strictly inside itself. Hénon's trapping quadrilateral with corners (-1.33, 0.42), (1.32, 0.133), (1.245, -0.14), (-1.06, -0.5), the image of its boundary under the Hénon map lying strictly inside it, and an orbit on the attractor.

A region the orbit cannot leave

That the Hénon map and the Lorenz flow have attractors takes two lines of arithmetic each — a region mapped strictly inside itself, a quantity that falls outside an ellipsoid. That the attractors are strange took a computer and twenty years for Lorenz, and for Hénon's classical parameters it has never been done. The difference between the two questions is the difference between a region and what lives in it.

dynamics · Strange attractor
Every three-state machine and what becomes of it. halt: 1379; no halting entry: 12492; exact repeat: 361; shifted repeat: 2254; dies backwards: 36; unexplained: 27.

The machines that need a reason never to stop

Run every three-state machine on a blank tape and the ones that halt announce themselves: the longest stops after 21 steps. The work is in the others. Each needs a reason it will never stop, and four simple kinds of reason settle all but 27 of them — machines that sweep back and forth over a growing tape and defeat every check that looks for a repeat.

logic · Diagonalisation
Two stable cycles a hair from the classical Hénon attractor. The Hénon attractor at a = 1.4 with the certified stable period-13 orbit at a = 1.39945 and period-19 orbit at a = 1.4001616 drawn over it.

Stable cycles a hair from Hénon's chaos

Nobody knows whether the Hénon map at a = 1.4 is chaotic, because a stable cycle in a window too thin to see would look exactly the same. So hunt the windows: a stable orbit of period 19 at a = 1.4001616, proved to exist and to attract by interval arithmetic, in a window 15 hundred-millionths wide and 0.00016 from the classical value — and nothing nearer, down to a spacing of a ten-billionth.

dynamics · Strange attractor

Named alongside it

The objects these essays reach for when they reach for this one.

Henon mapInterval arithmeticStrange attractorBifurcationBusy beaverCertificateChromatic numberDecidabilityEuler characteristicExhaustive searchGraphGraph colouring

All concepts