AI for Formal Math, and Physics, and why they're different

Alexander Meiburg examines how language models and interactive theorem provers are changing AI-assisted mathematics. Models can propose creative natural-language arguments but also make subtle errors; formal proof systems provide grounding. The talk discusses model development, strengths and weaknesses, and the differences involved in extending formal assistance to physics, where establishing suitable definitions can be a larger obstacle than proving statements.