Natural-language arguments

…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.

…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.