I remember attending a talk about Lean well before LLMs or the current AI craze. They were trying to automate mathematics for a long time.

While everything seems crazy right now, the building blocks have been coming together for a long time now.