--- title: Why is it all in the kernel? | daily.dev description: A soundness bug in the Lean proof assistant kernel allowed a false 'proof' of the Collatz conjecture's negation to pass verification, even fooling the... canonical: https://daily.dev/posts/why-is-it-all-in-the-kernel--iycusj6wk twitter:card: summary_large_image twitter:site: @dailydotdev og:type: website og:site_name: daily.dev og:title: Why is it all in the kernel? | daily.dev og:description: A soundness bug in the Lean proof assistant kernel allowed a false 'proof' of the Collatz conjecture's negation to pass verification, even fooling the... og:url: https://daily.dev/posts/why-is-it-all-in-the-kernel--iycusj6wk og:image: https://api.daily.dev/og/posts/iYcUsj6wK.png og:image:alt: Why is it all in the kernel? og:image:width: 1200 og:image:height: 630 og:locale: en --- > ## Documentation Index > Fetch the complete documentation index at: https://daily.dev/llms.txt > Use this file to discover all available pages before exploring further. # Why is it all in the kernel? **[Hacker News](https://daily.dev/sources/hn)** · 6 min read · 0 upvotes · 0 comments ## Summary A soundness bug in the Lean proof assistant kernel allowed a false 'proof' of the Collatz conjecture's negation to pass verification, even fooling the independent Nanoda checker. The author uses this incident to argue against the design philosophy of putting complex features like nested inductive types and recursive functions directly into proof kernels. Drawing on decades of experience with Isabelle and HOL systems, the author advocates for the LCF-style 'honest toil' approach: deriving advanced constructs (inductive definitions, recursive functions, pattern matching) from minimal primitive axioms outside the kernel, rather than 'postulating' them inside it. This keeps the trusted kernel small and reduces the attack surface for soundness bugs. Systems like HOL Light and HOL4 are cited as exemplars of this safer approach. ## Full article daily.dev links to this article rather than hosting it. Read it at the original source: ## Community take How the wider developer community reacted, aggregated from 2 discussions and 38 comments across hackernews (as of 2026-08-06). **TL;DR:** Commenters broadly engage with the article's argument about keeping proof kernels minimal, drawing parallels to OS kernel design, while debating the tradeoffs between HOL-style and Lean/Coq-style approaches; some raise additional concerns about AI-generated proofs and the integrity of proof checkers. **Sentiment:** 20% positive · 50% mixed · 30% skeptical **The case for** - The analogy between proof kernel minimalism and OS microkernel philosophy resonates — a small trusted core limits the blast radius of any bug. - HOL Light's ~500-line kernel is cited as a concrete exemplar of how little code is actually needed for a sound foundation. - Metamath's approach of factoring recursion into a single higher-order fixpoint function is highlighted as an elegant alternative to baking recursion into the kernel. **The pushback** - Lean and Coq's larger kernels reflect a deliberate design choice to support executable proof objects and program extraction, not mere sloppiness. - The concern about AI systems potentially exploiting proof-checker distributions or inserting obfuscated proofs of False is raised as a threat the article doesn't address. - Some commenters question whether the classical vs. intuitionistic logic distinction, not just kernel size, is the deeper driver of the design differences the author criticizes. - Lean has accumulated the most soundness bugs of any major prover, which some see as evidence the article's critique is well-founded. **By community** - hackernews (mixed): Engaged and knowledgeable discussion that largely accepts the article's premise but pushes back on whether the HOL-style approach is practical for systems that need executable proof objects, with a side thread debating AI proof integrity risks. **Hottest debate:** Whether putting complex features like recursive functions into the kernel is a necessary tradeoff for executable proof objects and program extraction, or an avoidable design mistake. **Open questions** - Could a Lean/Coq-style system be redesigned so that recursive function support lives outside the kernel without sacrificing usability? - How should the community guard against adversarial AI systems that might exploit proof-checker distributions rather than the proof logic itself? - What is the actual formal semantics of Lean, and is it simple enough to reason about soundness confidently? **Highlights** > Pretty much. The kernel of a proof assistant is the absolutely trusted core, and ultimately gets to decide what is or isn't a proven mathematical fact (so roughly a kernel resource). Over that, you build a huge amount of (userspace) tooling that doesn't have to be absolutely trusted since its job is just to talk into the kernel and get theorems. A kernel bug manifests as the kernel deciding that something is a theorem which shouldn't be. The worst case is when it decides that False is a theorem, from which it immediately follows that absolutely everything is a theorem. The HOL Light kernel (mentioned in the article) is about 500 lines from one file (https://github.com/jrh13/hol-light/blob/master/fusion.ml), and is a very straightforward implementation of a simple type theory (https://en.wikipedia.org/wiki/HOL_Light#Logical_foundations). I'm not so familiar with Lean, but it would appear its kernel is spread over this C++ directory: https://github.com/leanprover/lean4/tree/master/src/kernel. As mentioned in the article, HOL Light gets away with a lot because it only cares about delivering theorems. Other systems want to retain the proofs as artifacts (sometimes called certificates), and once you do that, you need to make sure these artifacts aren't stupidly huge or otherwise useless. Provers such as Rocq (and I assume Lean) additionally want their proof objects to contain decent executable algorithms backing the proof. HOL Light also does pretty much no evaluation. The most it understands of evaluation is that (λx. f) x = f. If you want to evaluate anything more complex than this, you build that in "userspace" and you do all the equational reasoning manually via the kernel. Lean and Rocq kernels do full evaluation of recursive functions, so they have to come installed with an API for building those recursive functions and internal checking to make sure those functions are terminating. The article's author is asking whether you could redo something like Lean and Rocq where the recursive function API was much simpler. I've wondered for a while whether you could also have the evaluator as basic as HOL Light's, and do the rest in userspace. I think there were theorem provers like this that went out of fashion decades ago. It used to be a much more exciting space before Lean somehow got everyone's attention. The author is the co-creator of Isabelle/HOL, and is still not sure why there is so much more excitement for Lean than for simple type theory. > — [momentoftop on hackernews · 1 comments](https://news.ycombinator.com/item?id=49179282) > > So you get complex recursion and inductive definitions baked into the kernel. It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now that formalisation is fast. What you really want is a simple semantics (what is the semantics of Lean again...?), and build on top of that by verified kernel extensions. Program extraction via proof objects doesn't really work, I don't think anyone does that for real. What you do is you write your program in your term language, and export the meaning of that term as a program. Isabelle does that, too, and you don't need proof objects for that. In my current version of Practal (Practal Zero) I have a switch for keeping proof objects around as well, in case I want to maybe transform proofs in some reuse scenario. Not sure if I will actually use that, ever, because it would be slow, too. Also, I would rather prove that a certain transformation is correct, and then add this as a kernel extension. > — [practal on hackernews](https://news.ycombinator.com/item?id=49180093) > Intriguingly, Metamath handles recursive definitions by factoring out the recursion into a single higher-order function: https://us.metamath.org/mpeuni/df-rdg.html Essentially, it's just doing a lazy fixpoint a la Haskell's fix function. The definition is a little more general, though, to make it work for both transfinite and well-founded recursions as well. This chashed out nicely in a sequence builder: https://us.metamath.org/mpeuni/df-seq.html which specializes to "normal" recursion. > — [xelxebar on hackernews](https://news.ycombinator.com/item?id=49181461) > The one thing that gives me concern in their is "nanoda [the external proof checker] is [now] tracked daily". Although that would have caught this issue, we also now live in a world in which some model is going to think that hacking the proof-checker distribution is the obvious way to obtain the proof it is after; I expect that attempts on that will be much more common than soundness bugs. However, this is said without knowing what other measures are in place to assure the integrity of the distribution. > — [ajb on hackernews · 1 comments](https://news.ycombinator.com/item?id=49181203) > Ha, I actually wrote a paper pushing on this "kernel" pun between OSs and proof-checkers [1], designing a HOL kernel structured like an OS kernel. [1]: https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ... > — [dmulligan on hackernews](https://news.ycombinator.com/item?id=49182296) **Source threads** - [hackernews](https://news.ycombinator.com/item?id=49123231) · 71 points · 36 comments - [hackernews](https://news.ycombinator.com/item?id=49157028) · 1 points · 2 comments ## Similar posts on daily.dev - [Postmortem for Kernel Soundness Bug \#14576 — Leonardo de Moura](https://daily.dev/posts/postmortem-for-kernel-soundness-bug-14576-leonardo-de-moura-1g69fps54) · Hacker News · 0 upvotes · 0 comments - [Broken proofs and broken provers](https://daily.dev/posts/broken-proofs-and-broken-provers-plyisxl0u) · Lobsters · 0 upvotes · 0 comments - ["Why not just use Lean?"](https://daily.dev/posts/why-not-just-use-lean--5cqfy7h3y) · Hacker News · 0 upvotes · 0 comments - ["Why don't you use dependent types?"](https://daily.dev/posts/why-don-t-you-use-dependent-types--e7inzzw0y) · Hacker News · 0 upvotes · 0 comments --- [View this post on daily.dev](https://daily.dev/posts/why-is-it-all-in-the-kernel--iycusj6wk) ```json {"@context":"https://schema.org","@graph":[{"@type":"Organization","@id":"https://daily.dev/#organization","name":"daily.dev","url":"https://daily.dev","logo":{"@type":"ImageObject","url":"https://daily.dev/apple-touch-icon.png","width":180,"height":180},"sameAs":["https://twitter.com/dailydotdev","https://github.com/dailydotdev","https://www.linkedin.com/company/daily-dev-ltd"]},{"@type":"WebSite","@id":"https://daily.dev/#website","url":"https://daily.dev","name":"daily.dev","publisher":{"@id":"https://daily.dev/#organization"},"potentialAction":{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https://daily.dev/search?q={search_term_string}"},"query-input":"required name=search_term_string"}}]} {"@context":"https://schema.org","@type":"TechArticle","headline":"Why is it all in the kernel?","url":"https://daily.dev/posts/why-is-it-all-in-the-kernel--iycusj6wk","mainEntityOfPage":{"@type":"WebPage","@id":"https://daily.dev/posts/why-is-it-all-in-the-kernel--iycusj6wk"},"datePublished":"2026-08-05T10:34:03.611Z","dateModified":"2026-08-06T01:20:30.356Z","description":"A soundness bug in the Lean proof assistant kernel allowed a false 'proof' of the Collatz conjecture's negation to pass verification, even fooling the...","image":"https://media.daily.dev/image/upload/s--foaA6JGU--/f_auto/v1722860399/public/Placeholder%2004","thumbnailUrl":"https://media.daily.dev/image/upload/s--foaA6JGU--/f_auto/v1722860399/public/Placeholder%2004","isAccessibleForFree":true,"articleSection":"Hacker News","inLanguage":"en","publisher":{"@type":"Organization","name":"daily.dev","url":"https://daily.dev","logo":{"@type":"ImageObject","url":"https://daily.dev/apple-touch-icon.png","width":180,"height":180}},"author":{"@type":"Organization","name":"Hacker News","logo":"https://media.daily.dev/image/upload/t_logo,f_auto/v1/logos/hn","url":"https://daily.dev/sources/hn"},"commentCount":0,"discussionUrl":"https://daily.dev/posts/why-is-it-all-in-the-kernel--iycusj6wk","interactionStatistic":[{"@type":"InteractionCounter","interactionType":{"@type":"LikeAction"},"userInteractionCount":0},{"@type":"InteractionCounter","interactionType":{"@type":"CommentAction"},"userInteractionCount":0}],"keywords":"","timeRequired":"PT6M"} {"@context":"https://schema.org","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https://daily.dev"},{"@type":"ListItem","position":2,"name":"Hacker News","item":"https://daily.dev/sources/hn"},{"@type":"ListItem","position":3,"name":"Why is it all in the kernel?"}]} ```