Where is mathematics going [video]
youtube.com
youtube.com
For me two of the main takeaways were, given that you can't write proofs without correct definitions and theorem statements, (1) LLMs can't be trusted to accurately write Lean definitions of mathematical objects or statements of theorems from the contemporary research literature (hence a new funded project to get humans to do more of this), (2) LLMs are getting good at writing Lean code.
Kevin didn't speculate about what happens next, but it is certainly looking like a verifiable domain.