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

As little as five years ago, the image of 'AI for Math' focused on specialty models that could discover interesting examples or constructions, for example, graphs with interesting parameters, where our intuition might be lacking but computer checking is simple. With large language models this has flipped: AI can now generate English proofs with novel ideas and often human-like intuition, but they are prone to tiny errors that computers cannot catch. I'll discuss how Interactive Theorem Proving software is reshaping this, where LLMs can ground their reasoning in rigorous verification. I will discuss both how these models are developed, what they find easy or hard, and what is required to apply this to the domain of physics as opposed to pure math -- in particular, why definitions, not proofs, are increasingly the obstacle to AI-assisted physics.