Note that the claims are about the kernel that computes the mesh intersection, not the web demo: While the kernel is formally verified, the UI and glue code (that call the kernel) are not. I once hit a bug that looked like there were holes in the resulting mesh: I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specification, to floats before sending them to the GPU. All geometry is happening inside the kernel, for which we know the specification holds.
This is really neat. I think CSG is one of the more intuitive ways to build 3d environments (especially 'indoor' ones). No geometry is ever destroyed in a proper CSG workflow. A hierarchy of brushes makes it possible to very rapidly iterate parameters like how long a hallway is or the time it takes to get from one objective to another. Often, you only have to apply a transform to a single brush to affect something that would take a non-CSG workflow an entire afternoon to recover from.
The current story with CSG around commercial game engines is pretty awful. Unity has some 3rd party options that can work well but they're also glitchy and don't integrate well with the other parts of the ecosystem. For a while I thinking about building my own CSG implementation but the exact things this project solved were what was stopping me. The EditorWindow integration stuff is not as scary to me (although it is painful). The advanced geometry and set operations is what kept me from trying. It appears that dragon has been (at least partially) slain.
This seems like very cool work. I'm sorry if I missed it: I'm still not sure how we go from verified proof (Great!) to an implementation (by LLM or by Human) which you're sure actually conforms to the proof? How do we know that the implementation maps precisely to the description within the proof?
Both the implementation and the proof are written in Lean.
In the files I reference here https://github.com/schildep/verified-3d-mesh-intersection#mi...
there are theorems about the function that does the mesh intersection computation.
The implementation is in the CSG/Impl folder. The proof is in the CSG/Proof folder. They are imported and tied together in the human reviewed file. Lean checks that these theorems in the human reviewed file are proven via the proofs.
The code generation for Lean is not AFAIK verified in any way. It uses C as a portable assembler, and uses too many fancy C constructs to be compiled by CompCert C, which is the only fully verified compiler.
So you can have the strange situation of proof that the Lean code is correct, but no way of proving that the running machine code corresponds with the same program.
There is also the problem of knowing whether the microprocessor works according to its spec, and I don't think we have anything public about modern multi core processors about that.
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.
I haven't actually used Lean or other proof assistants, so take this with a grain of salt, but I think the basic idea is to use (complicated) function argument and return types to "encode" the spec, and rely on the compiler's typechecking to detect spec violations.
To get the feel of this it might help to start with a simpler example: If you declare a function in ordinary old Java with return type int, the Java compiler will complain unless every path through that function returns either an int or something that can be converted to it (or throws). Lean is similar but uses a much more powerful type system called dependent types, which gives you extreme control over the values that are permitted in a type: For example, in Lean it's possible to define a type that consists of just the even integers, or even just the prime numbers. If you define such a PrimeNumber type, and then declare a function that returns a PrimeNumber, the Lean compiler will complain if the function could ever return a number that is not prime. IOW, if your function compiles with no errors, it is proven to always return a prime number.
I expect that OP's code defines a function named something like intersect(), and which takes 2 arguments of a type named something like Mesh, and returns not simply another Mesh but in fact a more complicated type: specifically, a Mesh that is somehow constrained to be a sub-mesh of each of the first and second arguments. Since mesh intersection is deterministic, I expect that this more complicated type will turn out to be inhabited by just a single value (mesh) -- similar to a type FortyTwo whose only value value is the integer 42. (I'm assuming here that a mesh can only be represented in one canonical way; this might not be true.) Then, Lean will complain at compile time if there exists any conceivable pair of input meshes for which the function would construct the wrong intersection.
> A human reviewer only needs to read 93 lines of formal specification and run the Lean checker to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-written implementation. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human.
I am curious about the approach as I find claims like this hard to believe. There is a theory behind proof kernels that they must be small because they have to be trusted and verifiable by a human. Otherwise the whole system breaks.
How does one trust an LLM generated kernel is proving the right things?
Maybe what you mean is that kernels of proof assistants must be small. Here I am referring to a geometry processing kernel (that is formally verified by a proof assistant). The implementation of the algorithm can be very long, the proof that it conforms to the spec can be very long. But lean checks the proof. And so you only have to trust the spec and that the lean proof assistant is correct.
In the 93 lines I assumed a reviewer already trusts that the kernel of the Lean proof assistants is correct. We have to trust somethings.
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 about that function.
Right, I’m thinking of the de Bruijin criterion applied to the generated kernel in this case. That generated kernel sounds large, and being generated, I’m curious as to why or how we don’t have to verify/understand it?
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.
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.
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).
Came here to ask about this too. I was doing CSG stuff in the early 2000's and got physically and mentally sick from the pure hell that floating point accuracy created for me. Literally led me to quit my job. Full crashout. iykyk
The runtime performance is most probably worse than yours. The goal of this project is a minimal specification that a reviewer can trust. See section in readme on performance and how it could be improved while still keeping formal guarantees, but would mean a reviewer having to trust axioms on floating point numbers:
https://github.com/schildep/verified-3d-mesh-intersection#pe...
On a readme style note, please spend more time explaining the algorithm and less time bragging on how amazing vibe coding is or how Lean has a zero trust proof.
I presume the new advance is claim that verified-3d-mesh-intersection is verified and not the claim that vibe coding can replace hand proofs or that the claim that lean4 can be correct without trusting llms.
One complication: For union the spec would look a little bit different than for intersection. I defined the solid associated to a mesh in a way that does not include the surface of the mesh itself. That works for the intersection. For union we would have:
I think it would not be hard to reduce the implementation and the proof of correctness to the intersection: There are some tricks which you can do like flipping the orientation of a mesh and putting a large cube that contains both meshes around it and then intersect these. (And then at the end doing the reverse trick.) Hopefully the implementation would not actually do this, but this construction could be used in the proof.
no lean background here so the proofs are over my head, but the framing makes sense to me. everything i've shipped that claude co-wrote, the thing that made me trust it was running it end to end, never reading it. having a checker do that part is a way better deal.
We could use floats internally and gain a lot of performance as I described in my response here: https://news.ycombinator.com/item?id=49085136.
With this we would still be able to handle special cases correctly.
If you mean, you want float in the interface, I think the picture would be the similar as I described there: You still need to fallback to higher precision for certain computations. But you would also not be able to return the outputs correctly, so we would need to think about how we want to describe this in the specification...
The issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point. It's great that it's verified, but not for the case that is practically meaningful. Unless it's implemented using hardware accelerated floating point, most of these algorithms are not sufficiently performant to be practically useful.
> The issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point.
You can go a very long way using discrete math though. I'm pretty sure it's doable to implement, say, a 3D slicer (to prepare layers/paths for 3D printing I mean) without using any floating point operation.
P.S: FWIW I was coding intros and demos using 3D effects on the Commodore Amiga and then on 386 PCs without using the 387 (the FP co-processor of the 386, when present). I'm not saying it's useful to play games in 4K: what I'm saying is that there are certainly applications where formally verified algos using integer math do make sense.
CSG on meshes isn't really where FreeCAD struggles or focuses. That's more BRep, which is a harder problem than CSG.
Blender used to struggle with boolean operations, though. Seems to have got much better some time in the last couple of years, but without knowing any of the backstory I don't know if they've bodged it into shape or would benefit from something proven.
I think this would need to be reimplemented for performance. But maybe the spec can be reused. As agents get better we might reimplement the same spec for performance with minimal human effort. (See notes regarding performance and floats in readme.)
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.
I learned working with the Isabelle proof assistant in a university course. There were weekly exercises and a group project at the end. (Actually proving things by hand, no LLM.) That really helped. Before that course it was also hard for me to get into this.
Other than that you can also read introductory material for set theory. There the meaning of all of the unicode symbols you can see in the spec should be explained.
Note that the claims are about the kernel that computes the mesh intersection, not the web demo: While the kernel is formally verified, the UI and glue code (that call the kernel) are not. I once hit a bug that looked like there were holes in the resulting mesh: I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specification, to floats before sending them to the GPU. All geometry is happening inside the kernel, for which we know the specification holds.
This is really neat. I think CSG is one of the more intuitive ways to build 3d environments (especially 'indoor' ones). No geometry is ever destroyed in a proper CSG workflow. A hierarchy of brushes makes it possible to very rapidly iterate parameters like how long a hallway is or the time it takes to get from one objective to another. Often, you only have to apply a transform to a single brush to affect something that would take a non-CSG workflow an entire afternoon to recover from.
The current story with CSG around commercial game engines is pretty awful. Unity has some 3rd party options that can work well but they're also glitchy and don't integrate well with the other parts of the ecosystem. For a while I thinking about building my own CSG implementation but the exact things this project solved were what was stopping me. The EditorWindow integration stuff is not as scary to me (although it is painful). The advanced geometry and set operations is what kept me from trying. It appears that dragon has been (at least partially) slain.
That's why I integrated manifold into godot engine for constructive solid geometry!
https://github.com/godotengine/godot-proposals/issues/9711
Thank you! CSG has made level prototyping more fun and fast in Godot for me.
This seems like very cool work. I'm sorry if I missed it: I'm still not sure how we go from verified proof (Great!) to an implementation (by LLM or by Human) which you're sure actually conforms to the proof? How do we know that the implementation maps precisely to the description within the proof?
Both the implementation and the proof are written in Lean. In the files I reference here https://github.com/schildep/verified-3d-mesh-intersection#mi... there are theorems about the function that does the mesh intersection computation. The implementation is in the CSG/Impl folder. The proof is in the CSG/Proof folder. They are imported and tied together in the human reviewed file. Lean checks that these theorems in the human reviewed file are proven via the proofs.
The code generation for Lean is not AFAIK verified in any way. It uses C as a portable assembler, and uses too many fancy C constructs to be compiled by CompCert C, which is the only fully verified compiler.
So you can have the strange situation of proof that the Lean code is correct, but no way of proving that the running machine code corresponds with the same program.
There is also the problem of knowing whether the microprocessor works according to its spec, and I don't think we have anything public about modern multi core processors about that.
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.
Oh yes, it is still a better situation. Although C compilers are quite buggy.
Since Lean can emit LLVM it might be more achievable to reach performant assembly without going via C. All sorts of interesting work in progress.
https://dl.acm.org/doi/10.1145/3192366.3192377
(I am rate limited to ~5 comments a day so not replying for ages is just a function of the HN gods on Mt Sunnyvale.)
I haven't actually used Lean or other proof assistants, so take this with a grain of salt, but I think the basic idea is to use (complicated) function argument and return types to "encode" the spec, and rely on the compiler's typechecking to detect spec violations.
To get the feel of this it might help to start with a simpler example: If you declare a function in ordinary old Java with return type int, the Java compiler will complain unless every path through that function returns either an int or something that can be converted to it (or throws). Lean is similar but uses a much more powerful type system called dependent types, which gives you extreme control over the values that are permitted in a type: For example, in Lean it's possible to define a type that consists of just the even integers, or even just the prime numbers. If you define such a PrimeNumber type, and then declare a function that returns a PrimeNumber, the Lean compiler will complain if the function could ever return a number that is not prime. IOW, if your function compiles with no errors, it is proven to always return a prime number.
I expect that OP's code defines a function named something like intersect(), and which takes 2 arguments of a type named something like Mesh, and returns not simply another Mesh but in fact a more complicated type: specifically, a Mesh that is somehow constrained to be a sub-mesh of each of the first and second arguments. Since mesh intersection is deterministic, I expect that this more complicated type will turn out to be inhabited by just a single value (mesh) -- similar to a type FortyTwo whose only value value is the integer 42. (I'm assuming here that a mesh can only be represented in one canonical way; this might not be true.) Then, Lean will complain at compile time if there exists any conceivable pair of input meshes for which the function would construct the wrong intersection.
> A human reviewer only needs to read 93 lines of formal specification and run the Lean checker to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-written implementation. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human.
I am curious about the approach as I find claims like this hard to believe. There is a theory behind proof kernels that they must be small because they have to be trusted and verifiable by a human. Otherwise the whole system breaks.
How does one trust an LLM generated kernel is proving the right things?
Maybe what you mean is that kernels of proof assistants must be small. Here I am referring to a geometry processing kernel (that is formally verified by a proof assistant). The implementation of the algorithm can be very long, the proof that it conforms to the spec can be very long. But lean checks the proof. And so you only have to trust the spec and that the lean proof assistant is correct.
In the 93 lines I assumed a reviewer already trusts that the kernel of the Lean proof assistants is correct. We have to trust somethings.
What I’m wondering about is why we don’t need to understand/verify the generated kernel and only the spec?
Is there an implicit trust we must put in that kernel?
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 about that function.
Think of Lean proofs as a kind of inductive proof where if you trust the kernel then you trust every proof the kernel says is true.
Right, I’m thinking of the de Bruijin criterion applied to the generated kernel in this case. That generated kernel sounds large, and being generated, I’m curious as to why or how we don’t have to verify/understand it?
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.
Ok, that's very cool. I don't yet grasp exactly how this deals with numerical stability - the one true enemy of mesh-based CSG operations
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).
Moving to exact predicates on top of floating point numbers would be a big speed boost. CGAL does this.
It uses exact rational numbers everywhere, represented as quotient of 2 unbounded integers.
Came here to ask about this too. I was doing CSG stuff in the early 2000's and got physically and mentally sick from the pure hell that floating point accuracy created for me. Literally led me to quit my job. Full crashout. iykyk
How does it compare against https://github.com/elalish/manifold in performance and zero corruption?
I spent a lot of time making elalish/manifold work in Godot Engine and it is now a method in Blender too.
https://manifoldcad.org
If it helps, feel free to use the apache2 licensed unit tests that were generated in manifold development https://github.com/elalish/manifold/tree/master/test
The runtime performance is most probably worse than yours. The goal of this project is a minimal specification that a reviewer can trust. See section in readme on performance and how it could be improved while still keeping formal guarantees, but would mean a reviewer having to trust axioms on floating point numbers: https://github.com/schildep/verified-3d-mesh-intersection#pe...
> Why we cannot have manifold output meshes in general
As far as I know manifold is not verified software, but it does promise that manifold inputs become manifold outputs.
I wonder how manifold will break in that condition or would it snap to the nearest manifold.
https://github.com/schildep/verified-3d-mesh-intersection#wh...
On a readme style note, please spend more time explaining the algorithm and less time bragging on how amazing vibe coding is or how Lean has a zero trust proof.
I presume the new advance is claim that verified-3d-mesh-intersection is verified and not the claim that vibe coding can replace hand proofs or that the claim that lean4 can be correct without trusting llms.
This is a really cool project. Love it. Why not extend to union, difference, and xor? Is that exercise left to the reader or is it not tractable? ;)
I'm also curious if you've consider fuzz testing this system to verify the results.
Good question!
One complication: For union the spec would look a little bit different than for intersection. I defined the solid associated to a mesh in a way that does not include the surface of the mesh itself. That works for the intersection. For union we would have:
solidWithSurface (meshUnion M₁ M₂) = solidWithSurface M₁ ∪ solidWithSurface M₂
I think it would not be hard to reduce the implementation and the proof of correctness to the intersection: There are some tricks which you can do like flipping the orientation of a mesh and putting a large cube that contains both meshes around it and then intersect these. (And then at the end doing the reverse trick.) Hopefully the implementation would not actually do this, but this construction could be used in the proof.
Regarding fuzzing. It cannot find the special cases I listed in the readme, because these cases are very rare.
Yet with formal verification we can prove that the implementation actually satisfies the specification for all of infinitely many possible inputs.
no lean background here so the proofs are over my head, but the framing makes sense to me. everything i've shipped that claude co-wrote, the thing that made me trust it was running it end to end, never reading it. having a checker do that part is a way better deal.
Would you still be able to deal with coplanar faces if you were to expand this to floats?
We could use floats internally and gain a lot of performance as I described in my response here: https://news.ycombinator.com/item?id=49085136. With this we would still be able to handle special cases correctly.
If you mean, you want float in the interface, I think the picture would be the similar as I described there: You still need to fallback to higher precision for certain computations. But you would also not be able to return the outputs correctly, so we would need to think about how we want to describe this in the specification...
The issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point. It's great that it's verified, but not for the case that is practically meaningful. Unless it's implemented using hardware accelerated floating point, most of these algorithms are not sufficiently performant to be practically useful.
It is possible to prove things involving floats, you just have to addionally trust a small set of axioms on floats. See https://github.com/schildep/verified-3d-mesh-intersection#pe... Don't know if there is something like this in Lean. But there is https://flocq.gitlabpages.inria.fr
There are plenty of proof systems that can handle floating point? The proof doesn't happen during execution...
> The issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point.
You can go a very long way using discrete math though. I'm pretty sure it's doable to implement, say, a 3D slicer (to prepare layers/paths for 3D printing I mean) without using any floating point operation.
P.S: FWIW I was coding intros and demos using 3D effects on the Commodore Amiga and then on 386 PCs without using the 387 (the FP co-processor of the 386, when present). I'm not saying it's useful to play games in 4K: what I'm saying is that there are certainly applications where formally verified algos using integer math do make sense.
Congrats with this achievement. Do you see it possible that this project can be integrated into, for example, FreeCAD?
CSG on meshes isn't really where FreeCAD struggles or focuses. That's more BRep, which is a harder problem than CSG.
Blender used to struggle with boolean operations, though. Seems to have got much better some time in the last couple of years, but without knowing any of the backstory I don't know if they've bodged it into shape or would benefit from something proven.
Blender uses the manifold library after years of petitioning
I think this would need to be reimplemented for performance. But maybe the spec can be reused. As agents get better we might reimplement the same spec for performance with minimal human effort. (See notes regarding performance and floats in readme.)
Does FreeCAD use triangle meshes? CAD is usually NURBS surfaces, which require similar algorithms but on curved surfaces.
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.
I learned working with the Isabelle proof assistant in a university course. There were weekly exercises and a group project at the end. (Actually proving things by hand, no LLM.) That really helped. Before that course it was also hard for me to get into this.
Other than that you can also read introductory material for set theory. There the meaning of all of the unicode symbols you can see in the spec should be explained.