

Multi-trillion-dollar (-self-valued) industry that’s the future of all work and that everyone who doesn’t use it gets left behind and everyone who does use it evokes superheroically productive turns out to be helpless in the face of a small group of outspoken and minimally organised opponents?
I see.
One of the things that’s never clear from the reporting on ai successes is exactly how much actual paid human time went in to achieving those successes. This was especially notable in the fable-based security work… a huge amount of person-hours went into turning fable-detections into actual meaningful vuln reports.
A lot of demonstrably clever and capable people are involved with the llms-for-maths work, and a lot of money was spent on their time and supporting their work. Replicating it without your own stable of mathematicians and computer scientists and all the tokens they can eat is probably impractical.
Fwiw, lean is a general purpose programming language, though despite microsoft’s efforts no-one uses it for that. I think its popularity with mathematicians came as a bit of a surprise.
Anyway, the other important thing that didn’t get reported on is that building the formal definition of the problem is not trivial! Obviously I don’t need to tell you that, but from the reporting you’d think that an llm solved all these problems, when in fact it was an llm in the hands of some very capable people who absolutely did not just prompt the thing in plain english.
Anyone hoping for self-marking homework here is going to be disappointed… lean slop confirming to formal spec slop is just expensive slop. Reviewing regular genai code is awful, even the thought of reviewing genai dependently-typed code makes me want a new career.