“A critical look at Lean4” by Milo Moses

Lots of the discussion around Lean certificates and trust centers around general philosophical ideas of how much humans should trust formal certificates. It's important to remember, though, that Lean4 is not an ideal formal certificate machine: Lean4 is a software in its infancy and has issues. There are reasonable reasons to specifically not trust Lean4. If we're going to be putting our society's trust in Lean4, I think that it's good to have an open critical discussion of how warranted that trust is. Epistemic status: Most of this work is a factual description about aspects of Lean4 and set theory. I am 85% sure that at most two of these factual descriptions are incorrect. I am 90% sure that, in the current version of Lean4 on Github, there exists a proof of the statement "True=False" that would be accepted with two little blue checkmarks (either by messing with the elaborator, compiler, kernel, or some other part of the Lean). I am 2% certain that we will soon be putting huge amounts of trust into Lean4 certificates produced by misaligned AIs, and that the human work we do as a community thinking about and fixing Lean4 in the next 24 [...] --- Outline: (01:23) The current status of things (02:48) What does it mean for Lean4 to be consistent? (04:25) Smart people make fundamentally inconsistent type theories all the time (05:29) The status of Lean4's consistency proof (07:44) Untamed recursion is bug-prone (09:55) "But doesn't con-leche give a proof?" (12:15) Using Lean4 safely (13:42) How much do we trust the agents? (14:49) Where do we go from here? The original text contained 1 footnote which was omitted from this narration. --- First published: October 9th, 2026 Source: https://www.lesswrong.com/posts/zHhGa3iQBQcdSifFL/a-critical-look-at-lean4-1 --- Narrated by TYPE III AUDIO. --- Images from the article: Apple Podcasts and Spotify do not show images in the episode description. Try Pocket Casts, or another podcast app.