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