Caltech talk: using Lean formal verification to make AI math reasoning trustworthy
Cohere · youtube · 2026-10-09
Cohere published a talk by Caltech PhD student Robert Joseph George (advised by Anima Anandkumar) on making AI's mathematical and scientific reasoning rigorously verifiable rather than merely convincing.
Key points:
- TorchLean: a framework for verified machine learning in Lean, covering neural-network execution, automatic differentiation, floating-point semantics, and NN verification
- FloatLib: formally verified floating-point arithmetic
- Frontier applications: recent progress on the Navier–Stokes and Euler equations, plus his own work on singularity formation and stability in the 3D Euler equations
- Vision: AI, numerical computation, and formal verification converging so AI becomes a genuine tool for mathematical discovery — proposing ideas, running large-scale computation, assisting proofs, and independently checking resulting claims
Supported by the Caltech Graduate Fellowship, Harmonic AI, and the DARPA expMath fund.
More from Research
- EA-VAE paper in IEEE T-PAMI fixes systematic uncertainty failures in VAEs — enzoferrante · 2026-10-10
- OpenAI reportedly solved 92 of the 500 most important open math problems in one GitHub push — altryne · 2026-10-10
- AI math is teleportation to a foggy summit: Cepelewicz's striking mountain metaphor — burny_tech · 2026-10-10
- Isola lays out the three main pushbacks to the PRH narrative his new paper answers — phillip_isola · 2026-10-10
- Three findings from Isola's new paper: global map, text-to-image translation, orthogonality — phillip_isola · 2026-10-10
- Isola's team shows a global orthogonal map aligns image and text embeddings without paired data — phillip_isola · 2026-10-10