Proofs

Michael Freedman’s momentous 1981 proof of the four-dimensional Poincaré conjecture was on the verge of being lost. The editors of a new book are trying to save it.

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

Even as mathematicians and computer scientists proved big results in computational complexity, number theory and geometry, computers proved themselves increasingly indispensable in mathematics.

For almost a century, the anonymous members of Nicolas Bourbaki have written books intended as pure expressions of mathematical thought.

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.

Computer scientists are trying to build an AI system that can win a gold medal at the world’s premier math competition.

Mathematicians have long grappled with the reality that some problems just don’t have solutions.

Emily Riehl is rewriting the foundations of higher category theory while also working to make mathematics more inclusive.

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