Kevin Buzzard - Where is Mathematics Going? (September 24, 2025) Discusses the state of the art in research mathematics practice, application of LLMs, proof assistants, and work towards combining the two.
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.
RossBencina•4mo ago
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.