4 ms·
Search for 24:07, about 3/4 down where Strogatz poses the question: "do you imagine ... there will be a time when the descendants of Lean will be able to teach
by rfreytag 4y ago
Search for 24:07, about 3/4 down where Strogatz poses the question: "do you imagine ... there will be a time when the descendants of Lean will be able to teach themselves math, rather than having human teachers creating libraries?"
- schoen 4y agoIt's interesting because Kevin Buzzard in this interview basically says that other people are interested in the application of AI to proof generation, but he's not so interested in that. But in an earlier Quanta article, he sort of said he was: https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921/ https://www.quantamagazine.org/at-the-international-mathemat... I guess the IMO work is more about having computers automatically apply known theorems and techniques to novel (but not, fundamentally, "unsolved"!) problems, while this interview alludes to the more difficult task of getting computers to solve unsolved mathematics problems, and discover proofs of interesting theorems from scratch?
- mhh__ 4y agoBuzzard as far as I'm aware is interested in finding mistakes in mathematical work by "real" (i.e. in his own words people doing topology rather than category theory) mathematicians, so that position makes sense.