It'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

It'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?