START pod: Pedro Nobre, Co-Founder, Cajal: “Scaling Formal Verification for Scientific Discovery”

The most valuable thing in AI won't be generating answers.It'll be knowing which ones are right.Right now AI writes code, solves problems, produces proofs. But there's no way to guarantee any of it is correct. Pedro Nobre is building that guarantee.Cajal sits at the intersection of formal verification and AI. They use Lean, a language that lets you formalize a statement and derive a proof that's either correct or incorrect. Binary. No ambiguity.The hard part: the space of possible proofs is combinatorially large. Humans somehow navigate it with strange inductive biases. Machines couldn't keep up.Then reinforcement learning changed what's possible. AI can now iterate against an infinite source of reward: mathematical correctness itself.The thesis: create a superintelligent mathematician, and you solve most problems.They're already working with frontier AI labs. Starting in quantum computing and finance. Software verification and cryptography next.🎙️ Pedro Nobre, Co-Founder, Cajal on Fondo START Pod‍01:37 Formal verification explained - verifying whether software or mathematics is correct02:24 We need to make sure what AI outputs is correct03:07 Why mathematical proof search is combinatorially difficult03:42 How reinforcement learning is changing theorem proving04:11 Why AI is suddenly solving harder math problems04:28 We already have access to a superhuman mathematician04:46 The future of checking whether all mathematics is actually correct05:42 Quantum information theory and applied verification research06:36 Smart contracts, specifications, and provably correct systems07:11 If you create a super intelligent mathematician, then you solve most problems.‍Check out caj.al