I'm also not entirely convinced that plugging a proof assistant into an agentic coding harness is quite as big a deal as many are making it out to be.

It just kind of feels like a Watson moment. 15 years ago a computer won at Jeopardy!, and that spurred plenty of AI hype. Which was understandable, because playing well at Jeopardy is something that requires a lot of intelligence when humans are doing it. But what actually happened is that Watson's developers figured out a really clever way to cheese it, no general intelligence required. So it was also a kind of gee-whiz technology that didn't live up to the hype. Most applications based on it failed to generate any ROI and have since been discontinued, IBM lost billions of dollars on the venture, and it's now been sold off to a private equity firm and is mostly forgotten.

None of that means that Watson wasn't a technically impressive, even revolutionary product. But the world is full of impressive inventions that nevertheless fail to justify what they cost to build and operate.