Computer-assisted proofs

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.