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 2 essays across 2 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

Named alongside it

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

Chromatic number Euler characteristic Graph Graph colouring Henon map Interval arithmetic Lorenz system Lyapunov exponent Lyapunov function Planar graph Planarity Strange attractor

All concepts