1. LLM inference is cheap compared to the cost of a bug, and you can use tools to automate the proof-work, as you said so yourself.

2. Why would it? The AI shouldn't load already completed proofs, only their type signatures (which are one liners). Sounds like you're projecting bad context management?

Caching only works until you change a deeply nested constant. Then you must wait 2 hours as Lean re-checks every transitive dependency of a massive simp-ridden codebase. Also, first time check time IS relevant to UI. Nobody wants to wait 2h to start using a library after they first download it. Perhaps you don't mind that but I do; that's the kind of bad UX that made me go for that design choice on Bend. Which again, may be wrong or may be right. But it was intentional.

Having a checker that is just fast by construction, regardless of caching, was a top design priority, and I weighted it over verbosity in a layer I believe nobody will be reading anyway.

> you can use tools to automate the proof-work, as you said so yourself.

The language doesn't appear to be designed around supporting existing tools (either by exporting to Why3 or manually interfacing with existing tools). I'm not against shipping the whole proof or storing it on a cache server, I'm against the idea of having a LLM write it all. Even having the LLM only write proofs for subprograms that take a long time for ATPs to prove would work.

For the example in the article, the LLM had to write it exactly once without any iteration and it proved in a second, which I assume was mostly startup time. Having a LLM write 442 lines instead, which I assume also needed some iteration, is a tough sell in comparison.

I think people don't have an intuition of LLM costs and the time saved by using it. Of course it costs but its obvious that it brings more in savings than it costs.