Topic: formal verification

Ken Ono surveys how AI systems contribute to mathematical discovery, research-level reasoning and formal verification. Examples include AI-guided searches, progress on longstanding problems and formalization in Lean. The talk also examines reliability, attribution, unequal access, education and the future role of mathematicians. It argues for using AI to extend exploration while retaining mathematical judgment and strengthening trust through machine-checkable proofs.

Rodolfo Reis Soldati presents a Lean formalisation of a corrected proof of the generalised quantum Stein lemma, which gives relative entropy an operational interpretation in quantum resource theories. Formal verification combines topology, analysis and operator algebra, exposes small imprecisions in the mathematical argument and motivates a sharper definition of a resource theory. The resulting foundations extend the Lean-QuantumInfo library and support broader collaborative formalisation of quantum physics.

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.