The problem with large chunks of AI-generated code is no longer just whether they compile. It is who is actually going to review them.

A project published by schildep pushes that question into 3D geometry. The repository contains a mesh-intersection algorithm written in Lean 4, with more than 1000 lines of implementation and roughly 60,000 lines of formal proof generated by agents.

The proposal is not to make a human read all of it. It is almost the opposite: shrink what the human has to understand to 93 lines of formal specification, then let Lean's checker verify that the implementation satisfies that contract.

For agentic development, that is a useful shift. Instead of only trying to increase the average quality of generated code, the project reduces the amount of code anyone has to trust by inspection.

The contract fits in 93 lines

The chosen operation is intersection between solids represented by triangle meshes.

The repository formalizes conditions for a well-formed mesh, including a watertight surface, coherent orientation, no degenerate triangles and no self-intersection, with a relaxation that allows some touching along edges or vertices.

The core specification then states, in effect, that the solid produced by meshIntersect must equal the set intersection of the two input solids.

That mathematical contract stays short because it does not enumerate every irritating geometric case. A vertex sitting exactly on a face, coplanar triangles, rays hitting edges, T-junctions and BVH boundary cases remain implementation problems.

Lean checks the general property instead.

The author says a reviewer can focus on four small definition files, 93 lines excluding comments, then run the checker. The thousands of generated lines behind them become something to verify mechanically rather than prose to approve by eye.

AI wrote the proofs too

The delightful paradox is that the proof code is not presented as clean or pleasant.

The repository reports about 60,000 lines of AI-written formal proofs. They may be ugly in structure, style or maintainability. As long as the Lean kernel accepts them without unexpected assumptions, they establish what the specification requires.

The author even provides commands for inspecting which axioms the important theorems depend on and for searching for escape hatches such as unsafe, opaque, extern or implemented_by.

Formal verification therefore does not erase trust. It moves trust toward a much smaller base: the proof checker, the formal definitions and the assumptions a reviewer explicitly accepts.

That is more interesting than merely saying a model produced a lot of code.

The result is slow

The repository is unusually explicit about its main bad tradeoff.

Intersecting two roughly 70,000-triangle Stanford bunny meshes takes 24 seconds single-threaded on an M4 Pro, according to the project's benchmark. The author says this is far slower than state-of-the-art mesh intersection software.

The project uses exact arithmetic and runtime well-formedness checks where production geometry libraries may use more aggressive floating-point and optimization strategies.

Its priority is different: minimize the human effort needed to establish correctness.

Not every useful property is formalized either. Runtime performance and triangulation quality beyond well-formedness remain outside the contract. A program can therefore be perfectly correct with respect to the specification while still being slow or producing more triangles than necessary.

The guarantee is never "this software is good." It is "this software satisfies the properties we successfully wrote down."

A C++ comparison finds three rare bugs

The repository includes another useful experiment.

The author asked Claude Opus 4.8 to implement the same operation in C++ from an informal specification. That version also reached more than 1000 lines and included tests.

A separate agent comparing the C++ kernel with the formally verified implementation identified three distinct bugs that the author says were reproduced on specific inputs. They involve rare geometric configurations, exactly the class of edge case that ordinary black-box testing struggles to cover exhaustively.

This is not a general benchmark of C++ versus Lean, and it does not prove every generated program should be formalized. Mesh intersection happens to be a problem with a compact mathematical specification.

The author makes the limitation explicit: many practical software problems do not admit such a simple contract.

The review unit may become the specification

Agentic coding creates an awkward asymmetry. An agent can generate 5000 lines while a human reviews 200.

The common response is to add review agents around the first agent. That improves coverage, but the chain remains probabilistic.

This experiment offers another kind of compression: have the human review the contract rather than the implementation.

It will not work everywhere. It can consume enormous amounts of agent time. Generated proof code creates its own debt. And a specification can simply omit the property that later matters most.

But the framing is useful. As code becomes cheaper to produce, the scarce resource is not typing. It is human ability to know what is actually being accepted.

In this project, 93 lines matter more than 61,000.