Episode
START pod: Pedro Nobre, Co-Founder, Cajal: “Scaling Formal Verification for Scientific Discovery”
- Podcast
- START
- Published
- May 20, 2026
- Duration seconds
- 578
- Processing state
not_requested- Canonical source
- https://share.transistor.fm/s/4a76c799
Actions
POST https://stenobird.com/v1/public/podcasts/start-7171926/episodes/start-pod-pedro-nobre-co-founder-cajal-scaling-formal-verification-for-scientific-discovery/transcription-requests
Idempotently request low-priority transcript generation for this episode.GET https://stenobird.com/podcast/start-7171926/start-pod-pedro-nobre-co-founder-cajal-scaling-formal-verification-for-scientific-discovery.md
Read the agent-friendly Markdown representation of this episode resource.
Summary
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 correct 02:24 We need to make sure what AI outputs is correct 03:07 Why mathematical proof search is combinatorially difficult 03:42 How reinforcement learning is changing theorem proving 04:11 Why AI is suddenly solving harder math problems 04:28 We already have access to a superhuman mathematician 04:46 The future of checking whether all mathematics is actually correct 05:42 Quantum information theory and applied verification research 06:36 Smart contracts, specifications, and provably correct systems 07:11 If you create a super intelligent mathematician, then you solve most problems. Check out caj.al