--- title: Show HN: Formally verified 3D CSG: Trust 93 lines spec,... description: A formally verified 3D mesh intersection (CSG) algorithm implemented in Lean 4, where correctness is guaranteed by 93 lines of human-readable specification... canonical: https://daily.dev/posts/show-hn-formally-verified-3d-csg-trust-93-lines-spec-not-1000-lines-ai-code-d0rpjy2h4 twitter:card: summary_large_image twitter:site: @dailydotdev og:type: website og:site_name: daily.dev og:title: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code | daily.dev og:description: A formally verified 3D mesh intersection (CSG) algorithm implemented in Lean 4, where correctness is guaranteed by 93 lines of human-readable specification... og:url: https://daily.dev/posts/show-hn-formally-verified-3d-csg-trust-93-lines-spec-not-1000-lines-ai-code-d0rpjy2h4 og:image: https://api.daily.dev/og/posts/d0RPJY2h4.png og:image:alt: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code 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. # Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code **[Hacker News](https://daily.dev/sources/hn)** · 17 min read · 0 upvotes · 0 comments ## Summary A formally verified 3D mesh intersection (CSG) algorithm implemented in Lean 4, where correctness is guaranteed by 93 lines of human-readable specification rather than trusting 1000+ lines of AI-written implementation. AI agents autonomously wrote over 60,000 lines of Lean proofs, which never need human inspection — the Lean type checker guarantees conformance at compile time. The project demonstrates a workflow where humans control only the specification while delegating implementation and proof to AI agents. A web demo lets users intersect STL meshes in-browser. Compared to a parallel AI-written C++ implementation, the formally verified version caught 3 distinct geometry bugs that black-box testing would almost certainly miss. Tradeoffs include slower performance (24s for two 70k-triangle Stanford bunnies) and higher token costs for proof generation. ## 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 1 discussion and 52 comments across hackernews (as of 2026-07-28). **TL;DR:** The community is genuinely impressed by the formal verification approach using Lean for a 3D mesh intersection kernel, with lively technical discussion about trust boundaries, floating-point limitations, and performance trade-offs. Most commenters engage constructively, though some raise legitimate concerns about practical applicability. **Sentiment:** 55% positive · 30% mixed · 15% skeptical **The case for** - Using Lean's proof checker means neither the AI-generated implementation nor the proofs need to be human-reviewed — only the 93-line spec does. - Exact rational arithmetic eliminates numerical stability issues that plague most CSG implementations. - The approach correctly handles rare geometric special cases that many implementations skip or cheat around. - Formal verification covers infinitely many possible inputs, something fuzz testing cannot achieve. **The pushback** - Performance is likely worse than existing solutions like manifold due to exact rational arithmetic instead of hardware floats. - The Lean-to-C code generation is not itself verified, and CompCert cannot compile it, leaving a gap between the proof and running machine code. - The README spends too much time on AI/vibe-coding claims rather than explaining the algorithm itself. - Floating-point inputs/outputs in the interface still require careful thought about how to express correctness in the spec. **By community** - hackernews (positive): Commenters are technically engaged and largely impressed, with substantive back-and-forth on proof trust boundaries, floating-point trade-offs, and practical integration potential. **Hottest debate:** Whether the trust placed in Lean's proof checker and the unverified C code generation is sufficient to call the overall system 'formally verified' end-to-end. **Open questions** - Can the spec be reused with a reimplemented, performant float-based kernel for practical use in tools like FreeCAD or Blender? - Is there a path to verifying the Lean-to-C compilation step, or at least narrowing the trusted computing base further? - How would the specification need to change to handle union, difference, and XOR operations? **Highlights** > You're confused because the word kernel is used in two different senses. The "generated kernel" refers to a "geometric modeling kernel", which has absolutely nothing to do with the proof-checking kernel that the de Bruijn criterion talks about. The proof can be verified by Lean's ordinary proof-checker, or external checkers. > — [saithound on hackernews](https://news.ycombinator.com/item?id=49086645) > The implementations uses exact rationals numbers. So there are no issues with numerical errors. We can do all geometrical operations exactly. Many performant implementations have a separate layer that tries to use floats to decide inequalities and fall back to higher precision when floats are not sufficient. As I understand, this layer can be separated from the geometrical predicates we need (what I mean by predicate is for example deciding which side of a plane a point is), so we could formalize that arithmetic layer separately using axioms on floating point numbers and then plug it in the existing code. I think we could do that and still provide exact outputs and prove the same spec we have right now and the performance should increase a lot, since most of the computations right now is computing all these predicates exactly. I would not say numerical stability is the one enemy of CSG. See the special cases https://github.com/schildep/verified-3d-mesh-intersection#sp... and bugs in an alternative C++ implementation that also used exact rationals mentioned in https://github.com/schildep/verified-3d-mesh-intersection#co.... Also note that many implementations don’t even try to treat special geometrical cases correctly (for example they „cheat“ by using something called simulation of simplicity which provides some guarantees against some bugs, but at the expense of not treating the cases exactly correctly which can lead to artifacts). > — [permute on hackernews](https://news.ycombinator.com/item?id=49085714) > Still, this is not a bad situation overall. If you are forced to trust the C compiler to correctly compile C, and the hardware to correctly implement the instructions in the documentation, well, you're already forced to trust both of those every day. So this doesn't give you an absolute proof of correctness. But it does substantially reduce the size of the problem, which is now limited to (1) verifying that you actually proved what you think you did, and (2) all the stuff you were normally trusting anyway. (Some of the stuff you were trust anyway is broken, of course.) But this is a smaller problem than trusting 1,000 lines of highly-optimized CSG code written by a model we don't actually understand. > — [ekidd on hackernews](https://news.ycombinator.com/item?id=49085475) > The implementation of a function is in the CSG/Impl folder. A proof is in the CSG/Proof folder. They are both imported and tied together in the human reviewed file in a theorem that makes a mathematical statement about the function. Lean checks mechanically that the theorems are proven via the supplied proofs. Here you have to trust the Lean checker, but neither the proof nor the implementation. Then you know that the statement in the file you reviewed holds. > — [permute on hackernews](https://news.ycombinator.com/item?id=49086390) > Honestly I think I'd have an easier time understanding 1000s of lines of slop than 93 lines of proofs lol. Does anyone have any recommended learning resources for this type of thing? Skimming the repo, it looks like a lot of unicode and math terminology, but this project seems really compelling to me. > — [bogwog on hackernews · 1 comments](https://news.ycombinator.com/item?id=49084815) **Source threads** - [hackernews](https://news.ycombinator.com/item?id=49083239) · 37 points · 52 comments ## Similar posts on daily.dev - [When AI Writes the World’s Software, Who Verifies It?](https://daily.dev/posts/when-ai-writes-the-world-s-software-who-verifies-it--tsppkfj9s) · Hacker News · 1 upvotes · 0 comments - [New tool lets users repair AI-generated 3D models, then fabricate them just the way they want](https://daily.dev/posts/new-tool-lets-users-repair-ai-generated-3d-models-then-fabricate-them-just-the-way-they-want-nofxwmqbf) · MIT News · 0 upvotes · 0 comments - [Prediction: AI will make formal verification go mainstream — Martin Kleppmann’s blog](https://daily.dev/posts/prediction-ai-will-make-formal-verification-go-mainstream-martin-kleppmann-s-blog-j1btzfnpe) · Lobsters · 2 upvotes · 0 comments --- [View this post on daily.dev](https://daily.dev/posts/show-hn-formally-verified-3d-csg-trust-93-lines-spec-not-1000-lines-ai-code-d0rpjy2h4) ```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":"Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code","url":"https://daily.dev/posts/show-hn-formally-verified-3d-csg-trust-93-lines-spec-not-1000-lines-ai-code-d0rpjy2h4","mainEntityOfPage":{"@type":"WebPage","@id":"https://daily.dev/posts/show-hn-formally-verified-3d-csg-trust-93-lines-spec-not-1000-lines-ai-code-d0rpjy2h4"},"datePublished":"2026-07-28T14:03:44.242Z","dateModified":"2026-07-28T17:44:41.022Z","description":"A formally verified 3D mesh intersection (CSG) algorithm implemented in Lean 4, where correctness is guaranteed by 93 lines of human-readable specification...","image":"https://media.daily.dev/image/upload/f_auto,q_auto/v1/posts/896f19487edd5018b88432a9c9100873?_a=AQAEuop","thumbnailUrl":"https://media.daily.dev/image/upload/f_auto,q_auto/v1/posts/896f19487edd5018b88432a9c9100873?_a=AQAEuop","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/show-hn-formally-verified-3d-csg-trust-93-lines-spec-not-1000-lines-ai-code-d0rpjy2h4","interactionStatistic":[{"@type":"InteractionCounter","interactionType":{"@type":"LikeAction"},"userInteractionCount":0},{"@type":"InteractionCounter","interactionType":{"@type":"CommentAction"},"userInteractionCount":0}],"keywords":"","timeRequired":"PT17M"} {"@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":"Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code"}]} ```