Computer-assisted proofs

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.