9 ms·

> 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 mani

• iFire 2mo ago
  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.
• elalish 2mo ago
  The difference is that my Manifold library uses a different definition of what constitutes a manifold mesh: https://github.com/elalish/manifold/wiki/Manifold-Library#manifoldness-definition https://github.com/elalish/manifold/wiki/Manifold-Library#ma.... By being a purely topological definition, there is no implicit assumption that vertices with the same coordinates are connected. As such we can still generate a 2-manifold even in the "impossible" cases. The more important difference though, is that our library can still handle epsilon-valid self-intersecting meshes, rather than just reporting an error. This is critical in practice because meshes are stored, transported, and transformed in floating-point, so even the formally-proven non-self-intersecting results of the library under discussion will not necessarily be valid input for it anymore after a round-trip through a file format or a rotation. Still, these are details. I think the real contribution here is demonstrating a new approach to formally verifying software even for notoriously difficult problems. I believe that concept is really important, as the general state of software reliability tells me that the state of the art in testing software is desperately lacking. I think formal verification may well be one of the most important aspects of computer science research in the nearish term.