--- title: Lean now ships with verified kernels | daily.dev description: Lean 4.35.0 ships with a new lake check command that exports and rechecks developments using leanchecker inside a sandbox, plus four new kernels: nanoda,... canonical: https://daily.dev/posts/lean-now-ships-with-verified-kernels-6wqkephwp twitter:card: summary_large_image twitter:site: @dailydotdev og:type: website og:site_name: daily.dev og:title: Lean now ships with verified kernels | daily.dev og:description: Lean 4.35.0 ships with a new lake check command that exports and rechecks developments using leanchecker inside a sandbox, plus four new kernels: nanoda,... og:url: https://daily.dev/posts/lean-now-ships-with-verified-kernels-6wqkephwp og:image: https://api.daily.dev/og/posts/6wQkEPhwP.png og:image:alt: Lean now ships with verified kernels 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. # Lean now ships with verified kernels **[Hacker News](https://daily.dev/sources/hn)** · 4 min read · 0 upvotes · 0 comments ## Summary Lean 4.35.0 ships with a new lake check command that exports and rechecks developments using leanchecker inside a sandbox, plus four new kernels: nanoda, lean4lean, con-leche, and con-ron. Con-leche is the first Lean kernel written in Lean and formally proven consistent (implemented and proven consistent by Claude models under supervision of Joachim Breitner at the Lean FRO), running at 0.69x the instructions of the official kernel on Mathlib. Con-ron is a Rust translation of con-leche verified with Aeneas to refine its checking algorithm, guarding against compiler/runtime bugs. lean4lean verification is expected within months. The post also flags scalability concerns as Lean developments grow toward billions of lines of code, requiring binary export formats and incremental checking. ## Full article daily.dev links to this article rather than hosting it. Read it at the original source: ## Questions this post answers ### What does the lake check command do in Lean 4.35.0? The lake check command exports a Lean development and rechecks it with leanchecker, the official Lean kernel stripped of extra tooling, running the whole process inside a sandbox. The sandbox can be disabled with the flag lake check --inadvisably-no-sandbox. A --paranoid mode also rechecks with four additional kernels: nanoda, lean4lean, con-leche, and con-ron. _Teams hardening proof pipelines can follow Lean kernel verification updates on daily.dev._ ### What is con-leche and how is it different from Lean's official kernel? Con-leche is the first kernel for Lean written in Lean itself and formally proven consistent, meaning every environment it accepts has a model in set theory based on Mario Carneiro's model of Lean's type theory. It was implemented and proven consistent by Claude models (Fable and Opus) under supervision from Joachim Breitner at the Lean FRO, and runs at 0.69x the instructions of the official kernel, checking all of Mathlib in about 100 seconds on eight threads. _Developers evaluating AI-assisted formal verification work can track these proofs on daily.dev._ ### How does con-ron protect against compiler bugs that con-leche might inherit? Con-ron is a Rust translation of con-leche, created by using AI to port the code and then using the Aeneas tool to prove the Rust version refines con-leche's checking algorithm. Since con-leche is formally proven consistent, any remaining unsoundness is likely a bug in Lean's own compiler or runtime, and it is very unlikely that the same bug exists in the Rust toolchain, so checking proofs with both kernels guards against that risk. _Anyone weighing cross-language verification strategies can follow these kernel designs on daily.dev._ ## Community take How the wider developer community reacted, aggregated from 1 discussion and 66 comments across hackernews (as of 2026-10-18). **TL;DR:** Most of the discussion drifts away from the kernel-verification release itself into a long debate about whether LLMs or Lean's formal rigor are driving recent math breakthroughs, with only a handful of comments addressing the actual technical content of verified kernels. **Sentiment:** 30% positive · 45% mixed · 25% skeptical **The case for** - Some see cross-checking a proof with multiple independently-implemented kernels (con-leche, con-ron) as a sound way to catch compiler/runtime-specific bugs. - Lean plus AI is seen as a strong combination, since Lean's precision complements AI's breadth of exploration. - Several commenters consider Lean a well-trusted, arguably the most trustworthy, proof assistant available. **The pushback** - Some call the verified-kernel announcement essentially a marketing post, noting it still rests on postulated set-theoretic assumptions and a simplified kernel. - Concerns were raised that both the Lean and Rust implementations might share bugs if they both rely on common bignum/arbitrary-precision arithmetic references. - Several argue formal Lean proofs weren't how progress actually happened — natural-language reasoning came first and Lean translation was a secondary, convincing step, undercutting claims about Lean's centrality. **By community** - hackernews (mixed): A small technical thread about the verified kernels is overshadowed by a much larger tangential debate on LLMs, mathematics, and whether Lean can be considered a foundational language for programmers. **Hottest debate:** Whether recent formalized-math breakthroughs are driven by Lean's rigor itself or mainly by LLMs' ability to deobfuscate/translate informal mathematical reasoning into formal proofs. **Open questions** - Does cross-checking with independently implemented kernels (Lean-based and Rust-based) meaningfully protect against shared underlying bugs, such as in arbitrary-precision arithmetic? - Is there a risk that proof verification efforts described as 'postulating set theory' understate the limitations imposed by Gödelian incompleteness in practice? - How exactly does the workflow of translating natural-language proofs into Lean proofs scale as developments grow toward billions of lines of code? **Highlights** > For the highlighted kernel (con-leche) , they postulate a set theory. Godel doesn't get involved because the proof is effectively saying Lean+ZFC entails Con(Lean), but even that isn't quite right, because the kernel doesn't include all the features of Lean. But even that isn't quite right, because they're actively modifying the kernel to be "simpler" to check. It's a marketing post at the end of the day is what I'm trying to say. Regardless, Lean is probably the most trustworthy proof assistant on the planet at this point. > — [voxl on hackernews · 2 comments](https://news.ycombinator.com/item?id=50138668) > > any remaining unsoundness bugs are most likely in Lean's compiler or runtime (including the bignum library). It is very unlikely that the same bug also exists in the Rust compiler or runtime, so by checking a proof with both con-leche and con-ron, you gain a high level of protection against this class of bugs An awful lot of references for arbitrary precision arithmetic are just repackaging Knuth’s explanations, so I wonder if there could in fact be a bug in common (Although you would like to assume every other piece of software using them would have also hit any issues by now, so maybe it is fine) > — [dwroberts on hackernews](https://news.ycombinator.com/item?id=50139193) > They created an implementation of a Lean kernel in Lean (con-leche) and verified it as consistent. Since there can be bugs in its compiler and runtime, they translated the code into Rust (con-ron), and verified the resulting kernel with another Rust-based verification tool. There is also an ongoing verification project of Lean4, which is written in Lean4 itself. (My mental model is Lean4 := Raku and Lean := Perl) So we have two verified kernels now, and another is awaiting release. > — [cloudbonsai on hackernews · 1 comments](https://news.ycombinator.com/item?id=50138012) > The proposal is that multiple checkers are unlikely to all have the same bugs so the more kernels you can use to check the results the more likely it is that the proof/code is consistent & correct (modulo set theoretic assumptions necessary for the correctness of the kernel). > — [measurablefunc on hackernews](https://news.ycombinator.com/item?id=50137748) > What’s more interesting to me is the fact that these two kernels (con-leche and con-ron) were actually implemented by Claude (with “human supervision”). Programming as a hand-crafted art is really diminishing fast. > — [cloudbonsai on hackernews](https://news.ycombinator.com/item?id=50139042) **Source threads** - [hackernews](https://news.ycombinator.com/item?id=50114758) · 179 points · 66 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 - [Lean proved this program was correct; then I found a bug.](https://daily.dev/posts/lean-proved-this-program-was-correct-then-i-found-a-bug--n0f0rtus1) · Lobsters · 0 upvotes · 0 comments --- Tags: [#rust](https://daily.dev/tags/rust), [#ai-coding](https://daily.dev/tags/ai-coding) [View this post on daily.dev](https://daily.dev/posts/lean-now-ships-with-verified-kernels-6wqkephwp) ```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":"Lean now ships with verified kernels","url":"https://daily.dev/posts/lean-now-ships-with-verified-kernels-6wqkephwp","mainEntityOfPage":{"@type":"WebPage","@id":"https://daily.dev/posts/lean-now-ships-with-verified-kernels-6wqkephwp"},"datePublished":"2026-10-18T05:19:38.458Z","dateModified":"2026-10-18T16:50:44.816Z","description":"Lean 4.35.0 ships with a new lake check command that exports and rechecks developments using leanchecker inside a sandbox, plus four new kernels: nanoda,...","image":"https://media.daily.dev/image/upload/s--HRgLpUt6--/f_auto/v1722860399/public/Placeholder%2003","thumbnailUrl":"https://media.daily.dev/image/upload/s--HRgLpUt6--/f_auto/v1722860399/public/Placeholder%2003","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/lean-now-ships-with-verified-kernels-6wqkephwp","interactionStatistic":[{"@type":"InteractionCounter","interactionType":{"@type":"LikeAction"},"userInteractionCount":0},{"@type":"InteractionCounter","interactionType":{"@type":"CommentAction"},"userInteractionCount":0}],"keywords":"rust,ai-coding","timeRequired":"PT4M"} {"@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":"Lean now ships with verified kernels"}]} {"@context":"https://schema.org","@type":"FAQPage","@id":"https://daily.dev/posts/lean-now-ships-with-verified-kernels-6wqkephwp#faq","mainEntity":[{"@type":"Question","name":"What does the lake check command do in Lean 4.35.0?","acceptedAnswer":{"@type":"Answer","text":"The lake check command exports a Lean development and rechecks it with leanchecker, the official Lean kernel stripped of extra tooling, running the whole process inside a sandbox. The sandbox can be disabled with the flag lake check --inadvisably-no-sandbox. A --paranoid mode also rechecks with four additional kernels: nanoda, lean4lean, con-leche, and con-ron. Teams hardening proof pipelines can follow Lean kernel verification updates on daily.dev."}},{"@type":"Question","name":"What is con-leche and how is it different from Lean's official kernel?","acceptedAnswer":{"@type":"Answer","text":"Con-leche is the first kernel for Lean written in Lean itself and formally proven consistent, meaning every environment it accepts has a model in set theory based on Mario Carneiro's model of Lean's type theory. It was implemented and proven consistent by Claude models (Fable and Opus) under supervision from Joachim Breitner at the Lean FRO, and runs at 0.69x the instructions of the official kernel, checking all of Mathlib in about 100 seconds on eight threads. Developers evaluating AI-assisted formal verification work can track these proofs on daily.dev."}},{"@type":"Question","name":"How does con-ron protect against compiler bugs that con-leche might inherit?","acceptedAnswer":{"@type":"Answer","text":"Con-ron is a Rust translation of con-leche, created by using AI to port the code and then using the Aeneas tool to prove the Rust version refines con-leche's checking algorithm. Since con-leche is formally proven consistent, any remaining unsoundness is likely a bug in Lean's own compiler or runtime, and it is very unlikely that the same bug exists in the Rust toolchain, so checking proofs with both kernels guards against that risk. Anyone weighing cross-language verification strategies can follow these kernel designs on daily.dev."}}]} ```