alt Hacker News> For example, I predicted about 15 years ago that AI would decisively beat humans at math, because math is formalizable. Most people didn't believe it until this summer, and some don't believe it still.
That is a laughable quote for anyone that know the history of type theory and the foundational crisis that happened at the beginning of the last century. Math as a whole can't be formalizable but we can create various formalist for different math purpose just like we have so much programming languages.
And the study and the creation of those formalisms is not something automatisable.
Replies
> And the study and the creation of those formalisms is not something automatisable.
Lol again. Have you tried it? Go ask your favorite LLM to invent a machine-checkable formalism for something that you vaguely describe to it. It'll oblige. If it's one of the top models and you give it a good budget, it'll do a good job. Very likely it'll do a better job than you.
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.