ImperialViolet’s Lean experiment is not just a formal-methods curiosity. It shows a different shape for AI-assisted programming: the model can search through proof attempts while the language runtime acts as a strict verifier.
The useful loop is simple: generate a proof, let Lean type-check it, inspect the failure, and try again. The model does not need to be right on the first attempt if the verifier is cheap, deterministic, and hard to fool.
That changes the cost model of dependent types. Historically, strong proofs demanded heavy proof engineering. In this setup, the expensive human step shifts toward choosing the invariant and keeping the implementation proof-friendly; the retry work can be pushed onto the model.
New Runtime read
The signal is structural because it gives agent systems a stronger success boundary than normal tests. Tests sample behavior. A type-checking proof can encode a universal property and reject whole classes of bugs.
This does not mean every program becomes Lean. The source is explicit about limits: performance can suffer, proof effort can scale poorly, and verified assembly did not scale in the author’s experiment. But it does show a new practical pattern for high-value components: use LLMs for search, use a verifier for acceptance, and keep the final artifact auditable.
For agent harnesses, this is the important part. The more deterministic the verifier, the more safely the model can be allowed to retry. Verification bandwidth becomes the scarce resource, and formal systems are one way to increase it.