Sign In

Communications of the ACM

ACM Opinion

Can Computers Be Mathematicians?

A robot contemplates math problems on a blackboard.

"I think that one of the things that's happening in this collaboration is that computer scientists are beginning to learn more about the nature of what modern mathematics actually looks like." -Kevin Buzzard

Credit: Getty Images

For the last few years, researchers and amateurs all over the world have worked together to translate the essential axioms of mathematics into a programming language called Lean. Armed with this knowledge, theorem-proving programs that understand Lean have begun helping some of the world's greatest mathematicians verify their work.

In an interview, Kevin Buzzard, professor of pure mathematics at Imperial College London, talks about the effort to "teach" math to Lean—and how projects like this one could shape the future of mathematics.

From The Joy of Why
View Full Article


No entries found