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?"
But in an earlier Quanta article, he sort of said he was:
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?