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
