Machine Learning Street Talk (MLST)

Joscha Bach is a cognitive scientist and the founder of the California Institute for Machine Consciousness.

SPONSOR:
---
Parallel is a single platform for all your agentic research: web search built for AI agents, with Pareto-optimal quality, cost and speed.
Get started: https://parallel.ai/mlst
---

Bach's null hypothesis is that consciousness is easy: an algorithm not much more complicated than the transformer, simple enough for an infant's brain to discover by itself. In this conversation with Tim, he lays out the Machine Consciousness Hypothesis in two parts. The first is that consciousness is a biological learning algorithm, the training algorithm that makes a brain like ours coherent. The second is that machines learning in self-organising ways might discover it in the same way. Either part can fail on its own.

From there they ask why there will never be a Turing test for consciousness, why a chess program is already a zombie, and why faking a mind can sometimes be harder than building one. The conversation runs through Leibniz's mill, the explanatory gap from John Searle to Thomas Nagel, Anil Seth's biological naturalism, integrated information theory and the letter that called it pseudoscience, Gödel and the limits of formal systems, and Mike Levin's idea that morphogenesis and the mind may run the same coherence algorithm. A tea-room interlude takes in Picbreeder and fractured, entangled representations. The episode closes on what it would take to convince us that a machine is conscious.

---

TIMESTAMPS:
0:00 Cold open: Could consciousness be a learning algorithm?
1:51 Introduction
3:37 What makes an agent?
6:16 Why consciousness needs explaining
14:57 Sponsor: Parallel
15:51 Leibniz's mill and causal patterns
24:21 Perceiving that you perceive
32:04 Two hypotheses, two ways to fail
40:42 Do minds converge?
49:23 Does consciousness converge too?
56:20 When language models reshape our thinking
59:16 Can simulated water make you wet?
1:09:21 Computation as construction
1:16:03 Error-correcting patterns and the Ruliad
1:22:28 Conscious, or simulating consciousness?
1:28:23 What would count as evidence?
1:35:49 The research programme

REFERENCES:
Joscha Bach, The Machine Consciousness Hypothesis (California Institute for Machine Consciousness)
Kumar, Clune, Lehman & Stanley, "Questioning Representational Optimism in Deep Learning: The Fractured Entangled Representation Hypothesis"
Giulio Tononi, integrated information theory
Fleming et al. 2023, "The Integrated Information Theory of Consciousness as Pseudoscience"
John Searle 1980, "Minds, brains, and programs", Behavioral and Brain Sciences
Kurt Gödel 1931, "On Formally Undecidable Propositions of Principia Mathematica and Related Systems"
Alan Turing 1950, "Computing Machinery and Intelligence"
Whitehead & Russell, Principia Mathematica
Paul Thagard 2022, "Energy requirements undermine substrate independence and mind-body functionalism"
Richard Sutton 2019, "The Bitter Lesson"
Michael Graziano, attention schema theory
Bernard Baars and Stanislas Dehaene, global workspace theory
Michael Levin 2022, "Technological Approach to Mind Everywhere", Frontiers in Systems Neuroscience
Chris Olah et al. 2020, "Zoom In: An Introduction to Circuits", Distill
Adele Lopez 2025, "The Rise of Parasitic AI", LessWrong

RESCRIPT:https://app.rescript.info/share/fc7088df0dc8b84200aa6e01c9a9ab6a

Kevin Hartnett is the author of *The Proof in the Code*.SPONSOR:---Cyber Fund built the Monastery to help founders ship products that were impossible a year ago. Applications for Batch 1 are now open.Apply now: https://cyber.fund---In 1998 Thomas Hales finished a proof of the Kepler conjecture that leaned so heavily on computer code that the Annals of Mathematics could not say whether it was true. That impasse opens Kevin Hartnett's book *The Proof in the Code*, and this documentary.Built around Tim's conversation with Hartnett, the film follows Lean from a side project at Microsoft Research to the system mathematicians now use to check their own field. Leonardo de Moura, Lean's creator, explains why everything rests on a small trusted kernel. Jeremy Avigad recalls the argument over foundations that changed Lean. Kevin Buzzard describes his fear that his corner of mathematics was becoming a house of cards, and Paul Lessard separates a correct proof from a useful one. Mathlib, Peter Scholze's Liquid Tensor challenge and Terence Tao's Equational Theories project all pass through.The second half turns to AI. AlphaProof, natural-language olympiad proofs and autoformalisation sharpen the question the book keeps asking: when a machine produces a proof nobody can read, what has actually been checked? The answer lies in the formalisation gap, the distance between the mathematics people mean and the statement a checker certifies. The film closes on the human story behind the software.---TIMESTAMPS:0:00 Cold open: proof, code and the wrong problem1:50 Kepler's oranges and the proof nobody could check6:54 How mathematicians decide a proof is true9:04 Correct is not the same as useful12:17 Sponsor: Cyber Fund12:53 What Lean is, and the small kernel it trusts15:23 From Microsoft's Z3 to Lean18:22 The argument over Lean's foundations24:52 One researcher versus a growing user base26:16 Kevin Buzzard's house of cards30:43 Mathlib as a barn raising37:16 The perfectoid-spaces stunt47:12 Scholze's proof nobody had read: Liquid Tensor53:20 Can AI learn to find proofs? AlphaProof58:43 AI mathematics in 2026 and Tao's experiment1:01:36 Lean's place in AI mathematics1:02:17 AI brute force versus the right abstraction1:05:19 Autoformalisation's Trojan horse1:07:25 The formalisation gap1:11:45 A proof is not understanding1:16:58 Integration hell and the zlib specification1:21:14 Verification in the AI software lifecycle1:22:38 The human story behind Lean1:31:09 The birthday walk1:33:05 Farewell---REFERENCES:[2:12] Thomas Hales, A proof of the Kepler conjecture (Annals of Mathematics, 2005)https://annals.math.princeton.edu/2005/162-3/p01[2:12] The Flyspeck project (the formal proof of the Kepler conjecture)https://github.com/flyspeck/flyspeck[12:53] Leanhttps://lean-lang.org/[30:43] Mathlibhttps://github.com/leanprover-community/mathlib4[30:43] Kevin Hartnett, "Building the Mathematical Library of the Future" (Quanta Magazine, 2020)https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/[47:12] The Liquid Tensor Experimenthttps://github.com/leanprover-community/lean-liquid[53:20] AlphaProof (Google DeepMind): AI achieves silver-medal standard solving International Mathematical Olympiad problemshttps://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/[59:23] The Equational Theories Project (Terence Tao)https://github.com/teorth/equational_theories[1:18:30] lean-zip (the zlib proof)https://github.com/kim-em/lean-zipFrontierMath Erdős (Epoch AI, 2026)https://epoch.ai/benchmarks/frontiermath-erdosBook: Kevin Hartnett, *The Proof in the Code* (Quanta Books, 2026)https://www.quantabooks.org/books/the-proof-in-the-code/---RESCRIPT: https://app.rescript.info/share/8604a0cd6ea4604a368028a05f4e6be4Support MLST on Patreon: https://www.patreon.com/mlstDiscord: https://discord.gg/HNnAwSduud

A lot of people in AI treat evolution as a dumb fallback, basically random search for when you can't take a gradient. Akarsh Kumar thinks that is wrong. Selection hangs on to partial solutions, so mutations only need to be useful about 1% of the time for the search to keep making progress.Akarsh is a PhD student at MIT working with Phillip Isola, works with Sakana AI, and is first author of the Fractured Entangled Representation paper with Kenneth Stanley, Jeff Clune and Joel Lehman. He tells Tim Scarfe why the path a learner takes may shape the structure of what it learns, and why that is a different way of looking at intelligence from the statistical one.Most of the conversation is about ASAL, the method he led for searching whole spaces of artificial worlds. Rather than predict what a rule will do, ASAL runs the simulation and asks a foundation model what happened. Mapped across all 262,144 Life-like rules, the most interesting worlds sit on one small island. Along the way: Game of Life, Lenia (with a clip from its creator, Bert Chan), neural cellular automata, Boids, Particle Life and the emergence of persistence.---TIMESTAMPS:00:00:00 Intro: artificial life, ASAL and Core War in four minutes00:04:19 Life as it could be, not just as it is00:05:46 Why the order you learn things in matters00:08:33 No shortcuts: Wolfram, novelty search and regularisation00:10:44 Kenneth Stanley: the path matters, not just the destination00:11:31 Statistical intelligence vs regularity-based intelligence00:13:49 Artificial chemistry and other possible universes00:15:59 Convergent patterns: shadows of the substrate?00:18:02 How Conway's Game of Life works00:20:49 Change one cell, change everything?00:22:31 Lenia (with Bert Chan) and neural cellular automata00:25:26 Boids, Particle Life and cell-like creatures00:28:47 Persistence, entropy and what life is00:30:15 ASAL: a foundation model as the critic00:34:04 Impostors inside the simulation00:36:50 From primordial soup to alien animals00:38:26 262,144 rules and the island of open-endedness00:40:17 From artificial life to AGI00:41:35 Core War: Game of Thrones, Turing edition00:43:22 LLMs as the mutation step: evolving warriors00:46:03 Evolution is anything but random---REFERENCES:paper:[00:04:19] ASAL (Kumar et al.)https://arxiv.org/abs/2412.17799[00:08:08] Assembly theory https://www.nature.com/articles/s41586-023-06600-9[00:09:54] FEP paperhttps://arxiv.org/abs/2505.11581[00:22:38] Lenia: Biology of Artificial Life (Bert Chan)https://arxiv.org/abs/1812.05433[00:23:20] Growing Neural Cellular Automata (Mordvintsev et al.)https://distill.pub/2020/growing-ca/[00:41:35] Digital Red Queen: Core War with LLMs (Kumar et al.)https://arxiv.org/abs/2601.03335[00:43:42] MAP-Elites https://arxiv.org/abs/1504.04909[00:44:55] AlphaEvolve https://arxiv.org/abs/2506.13131[00:47:03] AutoML-Zero (Real et al.)https://arxiv.org/abs/2003.03384book:[00:07:04] Why Greatness Cannot Be Planned (Stanley and Lehman)https://link.springer.com/book/10.1007/978-3-319-15524-1tool:[00:18:12] Conway's Game of Lifehttps://en.wikipedia.org/wiki/Conway%27s_Game_of_Life[00:25:27] Boids (Craig Reynolds)https://www.red3d.com/cwr/boids/[00:27:12] Particle Life (Tom Mohr)https://github.com/tom-mohr/particle-life[00:41:50] Core Warhttps://corewar.co.uk/other:[00:08:49] Computational irreducibility (Stephen Wolfram)https://www.wolframscience.com/nks/p737--computational-irreducibility/[00:10:46] MLST: Why Every AI Model Is an Impostor (Kenneth Stanley, FER documentary)https://www.youtube.com/watch?v=o1q6Hhz0MAg[00:28:30] MLST: Blaise Agüera y Arcas on life emerging from codehttps://www.youtube.com/watch?v=rMSEqJ_4EBk---LINKS:Akarsh Kumar: https://akarshkumar.com/ASAL project page and demos: https://pub.sakana.ai/asal/Digital Red Queen project page: https://sakana.ai/drq/RESCRIPT:https://app.rescript.info/public/share/Qfv3T0EVzqOXL_CYYeRr9Blv8HnNm4JsXBh7ByFjJbc

Tsung-Hsien (Shawn) Wen, CTO of PolyAI, tells Tim Scarfe why voice agents are harder than text agents. Voice adds time, and a good conversation depends on adapting to the person on the line, not just on reasoning to the best answer. Shawn describes an audio-native model (Dialog-RSN-1) that first predicts a turn-taking signal, then replies in text with citations, and writes the transcript last so enterprises can audit it.Along the way: training on real, noisy calls with synthetic noise added, and why over-cleaned audio made the new model worse. Latency, and what a voice agent should do while it thinks. Why a voice with a hint of regional accent beats a generic one. Why public benchmarks fall short for voice, why enterprises want to own their agent harness, and whether behaviour belongs in the harness or in the weights.The last stretch is about working with agents: cognitive debt, the shift from producing content to checking it, Wispr Flow, building tools that agents can use, and whether slop is in the eye of the reader.This episode was produced in partnership with PolyAI.https://poly.ai CHAPTERS0:00 Why voice agents are harder than text4:27 What enterprises want, and why PolyAI built its own model9:04 How an audio-native voice model works15:21 Training data, spectrograms and synthetic noise20:36 The cocktail party problem and the future of turn-taking25:21 Latency, adaptive reasoning and keeping callers' trust31:33 Voices, personality and the uncanny valley36:32 How do you benchmark a voice agent?42:00 Harness engineering and owning the intelligence45:09 Well-specified problems and auditable agents49:46 Weight adaptation and cognitive debt56:31 Agents at work: Wispr Flow, voice and tool building1:02:50 The next decade of voice, and what counts as slopREFERENCESThe Bitter Lesson: http://www.incompleteideas.net/IncIdeas/BitterLesson.html [9:05]Retrieval-augmented generation: https://arxiv.org/abs/2005.11401 [13:23]Mel scale: https://en.wikipedia.org/wiki/Mel_scale [17:16]Victor Zue: https://en.wikipedia.org/wiki/Victor_Zue [17:45]Cocktail party effect: https://en.wikipedia.org/wiki/Cocktail_party_effect [20:39]Speaker diarisation: https://en.wikipedia.org/wiki/Speaker_diarisation [21:16]

Leonardo de Moura created Lean and co-created Z3. ---This episode is sponsored by Parallel.Parallel, where agents find answers: web search, extraction and deep research APIs built for AI agents.Start free with the Parallel MCP server and $5 of credits every month: https://parallel.ai/mlst?utm_source=creator&utm_medium=podcast&utm_content=MLST---Tim Scarfe talks with Leo about how Lean escaped its original audience, why dependent types and Mathlib made it useful to working mathematicians, and what happens when formal verification leaves the lab. De Moura explains the small trusted kernel and independent checkers, and gives his account of the recent Collatz incident, in which a purported proof was accepted by both Lean's official kernel and Nanoda, apparently by exploiting a different bug in each.---TIMESTAMPS:00:00:00 Cold open: the green checkmark can lie00:00:59 Cathedral or bazaar: who controls Lean's core?00:04:55 Why Lean's core stays small and protected00:08:07 The Slack purge, Brandolini's law and the Lean FRO00:11:12 The Collatz exploit: two kernels, two bugs00:16:44 More kernels, reward hacking and safety by transparency00:21:04 Sponsor: Parallel00:21:59 Kim Morrison, Claude and the zlib proof00:25:25 Can we specify complex systems?00:28:04 Specs change: proofs are cheaper to redo with AI00:31:27 From Lean 1 to Lean 400:34:57 Dependent types in plain terms00:37:25 Lean 4's extensibility and Mathlib's growth00:41:44 Mathlib as infrastructure: Formal Frontiers00:44:15 Creativity, abstraction and nut-sniping00:48:46 Breadcrumbs, not learning: what AI agents lack00:53:03 Competence without comprehension, and verified guardrails00:56:21 Is the human still the author?01:01:44 AlphaProof, LLMs and why certificates still matter01:06:38 What's next for Lean, and its legacy01:11:42 How to start learning Lean---REFERENCES:tool:[00:00:48] Leanhttps://lean-lang.org/[00:01:24] Mathlibhttps://github.com/leanprover-community/mathlib4[00:12:09] nanoda_libhttps://github.com/ammkrn/nanoda_lib[00:12:19] CollatzLeanhttps://github.com/xrchz/CollatzLean/blob/a79357462a33d2a6babd4cf6c8d8bcd25425d653/README.md[00:13:06] Lean issue 14576https://github.com/leanprover/lean4/issues/14576[00:13:21] Lean pull request 14577https://github.com/leanprover/lean4/pull/14577[00:13:45] nanoda_lib pull request 22https://github.com/ammkrn/nanoda_lib/pull/22[00:15:33] Lean comparatorhttps://github.com/leanprover/comparator[00:18:02] Lean4Leanhttps://github.com/digama0/lean4lean[00:19:50] ARC-AGI-3https://arcprize.org/arc-agi/3[00:21:59] lean-ziphttps://github.com/kim-em/lean-zip[00:29:45] CompCerthttps://compcert.org/[00:29:45] seL4https://www.sel4.org/[00:30:23] Z3https://github.com/Z3Prover/z3[00:38:10] Veilhttps://github.com/verse-lab/veil[00:38:10] Velvethttps://github.com/verse-lab/velvetorganization:[00:00:52] Lean FROhttps://lean-lang.org/fro/[00:42:39] Mathlib Initiativehttps://mathlib-initiative.org/about/person:[00:05:11] Ilya Sergeyhttps://ilyasergey.net/[00:10:31] Joachim Breitnerhttps://www.joachim-breitner.de/[00:32:58] Adam Chlipalahttps://adam.chlipala.net/[00:38:42] Kevin Buzzardhttps://www.ma.imperial.ac.uk/~buzzard/[01:10:16] Terence Taohttps://terrytao.wordpress.com/book:[00:08:19] The Proof in the Codehttps://us.macmillan.com/books/9780374620059/theproofinthecode/other:[00:10:05] Brandolini's lawhttps://en.wikipedia.org/wiki/Brandolini%27s_law[00:45:33] A new result on unit distanceshttps://openai.com/index/model-disproves-discrete-geometry-conjecture/[01:01:08] Fermat's Last Theorem formalisationhttps://imperialcollegelondon.github.io/FLT/paper:[00:34:36] The Lean 4 theorem prover and programming languagehttps://doi.org/10.1007/978-3-030-79876-5_37---RESCRIPT:https://app.rescript.info/share/7d3d4a0059443236a01f6c9acbf4db58https://app.rescript.info/api/public/sessions/b007264c0ce89047/pdf