permute

6 ms·

1.
by permute 2mo ago
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
2.
by permute 2mo ago
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 functio
3.
by permute 2mo ago
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
4.
by permute 2mo ago
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 intersec
5.
by permute 2mo ago
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 inequalit
6.
by permute 2mo ago
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 m
7.
by permute 2mo ago
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 intersec
8.
by permute 2mo ago
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
9.
by permute 2mo ago
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 someth
10.
by permute 2mo ago
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 tha
11.
by permute 2mo ago
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 guarantee
12.
by permute 2mo ago
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
13.
Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code(github.com)
115 points by permute 2mo ago|49 comments
14.
by permute 3mo ago
There are two things here: The proof and how you would represent that in a program that you actually can run. From the math side, I am confident that the construction and proof can be extended to the real numbers and that can be formalized
15.
by permute 3mo ago
Yes, it runs significantly longer. Opus 4.8 ran autonomously for about 8 hours to provide program and proof of correctness, given the formal specification. And in previous experiments, Opus 4.7 failed and I was only able to do it using that
16.
by permute 3mo ago
Sure, what the program does is not interesting by itself, neither is that you can use AI to create programs to do polygon intersection. The main feature, that I hope is interesting in this submission, is that the program is formally verifie
17.
by permute 3mo ago
Yes
18.
by permute 3mo ago
Thanks! Yes, I hope AI and Lean will enable formally verified practical software.
19.
by permute 3mo ago
Thanks for the pointer, I will look into it. I think to do efficient formally verified geometry with floating point we would also need something like Shewchuk robust predicates. (I worked with them in the past to write robust software that
20.
by permute 3mo ago
Thanks! I am currently working on a follow up project for 3D polyhedrons for which the case handling really starts to get tedious. It's nice when AI can handle it without humans having to read the code and many unit tests to trust it.
21.
by permute 3mo ago
Yes, the webassembly is compiled from lean. The JS UI that calls the webassembly is not built from lean and not formally verified. So a human reviewer that does not trust the code, needs to review the formal spec and the UI code. But the ge
22.
by permute 3mo ago
Yes, the core supports exact rationals. This is easier to deal with in formal verification than floating point. I made the UI snap to a fixed precision, such that its easy to reproduce special cases with overlapping edges, coinciding vertic
23.
Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed(github.com)
93 points by permute 3mo ago|21 comments
24.
by permute 4mo ago
I am using Claude Code for formal verification with Lean. In my personal experience both Opus 4.7 and now what I see from first experiments with Opus 4.8 were big improvements. I was able to delegate proofs of larger theorems that their pre
25.
by permute 4mo ago
It’s fun to play around with this! It could be helpful to add support for parentheses and chaining of commands. For example: \add (\area-circle circ0) (\area-circle circ1). Intermediate nodes could be anonymous or automatically named.