Lean

2022年6月29日

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.

2021年7月28日

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,…

2021年6月21日

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…

2021年6月18日

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…

2020年10月20日

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,…

2020年9月21日

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…