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

Page: https://stenobird.com/podcast/start-7171926/start-pod-pedro-nobre-co-founder-cajal-scaling-formal-verification-for-scientific-discovery
Text version: https://stenobird.com/podcast/start-7171926/start-pod-pedro-nobre-co-founder-cajal-scaling-formal-verification-for-scientific-discovery.md
Podcast: [START](https://stenobird.com/podcast/start-7171926)
Published: 2026-05-20T19:10:52+00:00
Episode link: https://share.transistor.fm/s/4a76c799
Audio file: https://media.transistor.fm/4a76c799/0798ee6e.mp3
Processing state: not_requested
JSON: https://stenobird.com/v1/public/podcasts/start-7171926/episodes/start-pod-pedro-nobre-co-founder-cajal-scaling-formal-verification-for-scientific-discovery
Duration seconds: 578

## Resource

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

## Actions

- request_transcript: `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.
- read_markdown: `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.

A page view does not enqueue transcription. Agents should invoke `request_transcript` explicitly when they need this episode processed.

## Transcript

Full transcripts are not published on public pages unless there is a clear rights basis.