43:I[185,["/_next/static/chunks/08z4tkzvltetr.js","/_next/static/chunks/121~yigv24_j6.js","/_next/static/chunks/0jo3du-icy6v2.js","/_next/static/chunks/15cy49d~_zsjj.js","/_next/static/chunks/0..ktetnpeix7.js","/_next/static/chunks/0_htf5~kl..m1.js","/_next/static/chunks/0i6hzvr84kc1r.js"],"SendEmailButton"] 45:I[63625,["/_next/static/chunks/08z4tkzvltetr.js","/_next/static/chunks/121~yigv24_j6.js","/_next/static/chunks/0jo3du-icy6v2.js","/_next/static/chunks/15cy49d~_zsjj.js","/_next/static/chunks/0..ktetnpeix7.js","/_next/static/chunks/0_htf5~kl..m1.js","/_next/static/chunks/0i6hzvr84kc1r.js"],"AddToLibraryButton"] 46:I[29721,["/_next/static/chunks/08z4tkzvltetr.js","/_next/static/chunks/121~yigv24_j6.js","/_next/static/chunks/0jo3du-icy6v2.js","/_next/static/chunks/15cy49d~_zsjj.js","/_next/static/chunks/0..ktetnpeix7.js","/_next/static/chunks/0_htf5~kl..m1.js","/_next/static/chunks/0i6hzvr84kc1r.js"],"ShareButton"] 47:I[58016,["/_next/static/chunks/08z4tkzvltetr.js","/_next/static/chunks/121~yigv24_j6.js","/_next/static/chunks/0jo3du-icy6v2.js","/_next/static/chunks/15cy49d~_zsjj.js","/_next/static/chunks/0..ktetnpeix7.js","/_next/static/chunks/0_htf5~kl..m1.js","/_next/static/chunks/0i6hzvr84kc1r.js"],"ProcessEpisodeButton"] 48:I[45269,["/_next/static/chunks/08z4tkzvltetr.js","/_next/static/chunks/121~yigv24_j6.js","/_next/static/chunks/0jo3du-icy6v2.js","/_next/static/chunks/15cy49d~_zsjj.js","/_next/static/chunks/0..ktetnpeix7.js","/_next/static/chunks/0_htf5~kl..m1.js","/_next/static/chunks/0i6hzvr84kc1r.js"],"SignupCTA"] 3b:["$","time",null,{"dateTime":"2025-04-30T01:29:15.000Z","children":"April 30, 2025"}] 3c:["$","span",null,{"aria-hidden":true,"children":"·"}] 3d:["$","span",null,{"children":"02:50:53"}] 44:T52f,

Alok Singh researches provable AI safety via formal verification using Lean at Max Tegmark’s Beneficial AI Foundation, and writes about mathematics at alok.github.io.

0:00 - Intro

1:12 - Typing

8:45 - Elon’s demo day

22:42 - Animation, discrete vs continuous

29:04 - Number systems

35:26 - Nonstandard analysis

43:04 - Reasoning models and o3

50:45 - Fiction

55:48 - o1 and Linguistics

58:50 - Hyperfinite sets

1:11:58 - AI for math

1:16:01 - The field with one element

1:23:17 - Lean

1:31:53 - Lean for formally verifying superintelligence

1:36:03 - Ayn Rand

1:47:46 - Erewhon

1:57:56 - Proto-Indo-European

2:03:18 - More Erewhon

2:14:41 - Butler and Kaczynski

2:50:19 - Outro

Alok’s Website: https://alok.github.io/

Alok’s Twitter: https://x.com/TheRevAlokSingh

Beneficial AI Foundation: http://beneficialaifoundation.org/

Lean: https://lean-lang.org/

Transcript: https://www.theojaffee.com/p/podcast-alok-singh

More Episodes

YouTube: https://tinyurl.com/57jr42wk

Spotify: https://tinyurl.com/mrxkkhb4

Apple Podcasts: https://tinyurl.com/yck8pnmf

My Twitter: https://x.com/theojaffee

My Substack: https://www.theojaffee.com