>>16704963Fine, I'll bite. He's using it because it's useful and it's the way professional mathematician will be doing research in the future (5 years from now or less). If you consider the generation being born now won't have any idea what the world was like before AI and will be reliant on it, you can extrapolate that in 20 years doing research in math with an AI assistant + Lean will become the standard.