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 is not formally verified. Did not read up, if there is a formally verified library for them.) Shewchuk robust predicates give certain consistency guarantees that are nice to have when implementing computational geometry with floating points and I think can be formalized.
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.
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 geometry with rare special cases that we want to treat correctly happens in the verified core.
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 vertices etc. that make up much of the complexity of the algorithm.
In a past life i tried to implement Delaunay triangulation in floating point for data that can come in a rotated square grid. Normal precision doesn't work in that case. I learned a lot about arbitrary precision numbers doing that. The question about floats here gave me flashbacks.
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 predecessors could not handle.
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.
reply