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