Communications of the ACM
Can Computers Be Mathematicians?
"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