Lean

June 29, 2022

Artificial intelligence has bested humans at problem-solving challenges like chess and Go. Is mathematics research next? Steven Strogatz speaks with mathematician Kevin Buzzard to learn about the effort to translate math into language that computers understand.

July 28, 2021

Computer proof assistants have been an intriguing subplot in mathematics for years — promising to automate core aspects of the way mathematicians work, but in practice having little effect on the field. But a new result, completed in early June,…

June 21, 2021

If computers can beat us at chess, maybe they could beat us at math, too. Most everyone fears that they will be replaced by robots or AI someday. A field like mathematics, which is governed solely by rules that computers…

June 18, 2021

Proof-assistant software handles an abstract concept at the cutting edge of research, revealing a bigger role for software in mathematics. Peter Scholze wants to rebuild much of modern mathematics, starting from one of its cornerstones. Now, he has received validation…

October 20, 2020

Every day, dozens of like-minded mathematicians gather on an online forum called Zulip to build what they believe is the future of their field. They’re all devotees of a software program called Lean. It’s a “proof assistant” that, in principle,…

September 21, 2020

Computer scientists are trying to build an AI system that can win a gold medal at the world’s premier math competition. The 61st International Mathematical Olympiad, or IMO, begins today. It may go down in history for at least two…