“Math is hard. This is the problem. And it’s hard in several different distinct ways. I mean, one thing we’re doing right now is we’re teaching the computer scientists just how deeply hard mathematics is.”
– Kevin Buzzard.
Read or listen to the interview here
In 1997, DeepBlue developed by IBM, beat Garry Kasparov, the number one global chess player at the time. Could computers replicate this victory in the field of Mathematics research? Could they “out-think” the best human mathematicians?
Not yet, but maybe?
Steve Strogatz speaks with Kevin Buzzard, professor of pure mathematics at Imperial College London, on The Joy of Why, a podcast from Quanta Magazine about Lean, a programming language at the center of an effort to translate mathematical axioms into a language the computer can understand.
Lean is a tool being worked with, worked in, and worked on. Lean knows about integers and basic operations. A small but growing number of mathematicians and computer scientists are developing tactics, higher level abstractions that “make it seem you are communicating with a smart undergraduate, not a rigid machine.” Mathematicians are creating these support Math libraries. And computer scientists are writing theorem-proving programs in Lean.