The recent autonomous solution to the Navier-Stokes millennium problem was an extraordinary breakthrough. Yet, equally remarkable is how the global community accepted this solution without traditional, years-long peer review. This speed was possible because the proof included an autoformalized Lean certificate, allowing it to be mechanically verified. Lean was the foundational trust substrate beneath the discovery.

In this talk, I will explore the computational and social trust substrates that I expect to be essential for the future of AI-driven science. I will talk about AlphaProof Nexus, a system from my team at DeepMind that we announced in May 2026, and which served as the first large-scale demonstration of autonomous formal proofs for research-level mathematical theorems. I will also speak about Lean’s CSLib, an ongoing community effort to build a library of formalized computer science knowledge in Lean.

https://upenn.zoom.us/j/97645937545

Meeting ID: 976 4593 7545