Computer-assisted proofs

The “packing coloring” problem asks how many numbers are needed to fill an infinite grid so that identical numbers never get too close to one another. A new computer-assisted proof finds a surprisingly straightforward answer.

The four-color problem is simple to explain, but its complex proof continues to be both celebrated and despised.

Mathematicians using the computer program Lean have verified the accuracy of a difficult theorem at the cutting edge of research mathematics.

A small community of mathematicians is using a software program called Lean to build a new digital repository. They hope it represents the future of their field.

AI tools are shaping next-generation theorem provers, and with them the relationship between math and machine.

By translating Keller’s conjecture into a computer-friendly search for a type of graph, researchers have finally resolved a problem about covering spaces with tiles.