Topic: natural-language arguments

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.

Carina Hong discusses building systems for mathematical reasoning and machine-verifiable proofs. The conversation explores Lean, the scarcity of formal mathematical training data, and translating natural-language arguments into formal statements. It also examines conjecture-and-proof self-play and applications of formal verification to software and hardware.