Code nobody read, that you can trust anyway↗ (external link)

This is the most interesting thing I have linked all week, and it is a polygon library.

Multipolygon intersection, formally verified in Lean 4. The author states plainly that the implementation and the proofs were written autonomously by agents and never reviewed by any human, including him. Opus 4.5 through 4.8, with the later model able to formulate and execute large proof strategies on its own.

So why is this not the horror story it sounds like?

Because of what a human does review: three specification files, eighty-seven lines of Lean, defining polygon interiors by ray-casting parity. That is the entire trusted surface. If those eighty-seven lines say what you meant, then the Lean checker guarantees the implementation satisfies them — for every input configuration, not for the cases someone thought to test. The implementation is more than twice that size and considerably harder to follow, and it does not matter, because nothing rests on a human understanding it. As the README puts it, trust comes from the checker and a small specification, not from the model.

Sit with that, because it is a genuine answer to the problem this site keeps circling. Every other route out of the verification bottleneck has been about making review faster — better diff tools, AI reviewers, risk scoring. All of them are still asking a human to look at generated code and decide. This changes what gets reviewed: not the code, but a statement of what the code must be true of, in a form a machine can check exhaustively.

The catch is the obvious one. It works here because "these two polygons intersect correctly" is expressible in eighty-seven lines of maths. Write the specification for your billing system and see how far you get. The domains where this applies — geometry, parsers, compilers, crypto primitives, data structures — are exactly the domains where formal methods already worked, and the contribution is that the expensive part, the proofs, has got dramatically cheaper.

That is not nothing. That is the barrier that kept formal verification out of industry for forty years, and a model in a loop with a proof checker just walked over some of it. If the specification-writing gets easier too, this stops being a niche result.