Yes, this is how it would work. This has been attempted essentially since scientific thought has existed. The less “deterministic” fields exist because the approach you mention has not worked for hundreds of years.
Indeed. The people who suggested the change in 2021 and the mailing list threads have been purged from the search engines, but this thread is still here:
Talia Ringer, the main proponent, now writes posts that AI will turn out OK (and works on proof automation for programs so that more software engineers can become unemployed):
Remember that when you live under a bridge after having been fired that the world is fine because the great social injustice of the "Coq" name has been eradicated!
I don't know, what if someone made an app or a website where you get a dollar for every bit until an odd prime hits. The theorem says how much to price each spin to guarantee a long-term profit for the house (somewhere between tree fiddy and half a quadrillion dollars).
Actually, nothing practical, just sharing my love of math and excitement about the new possibilities of formal verification being unlocked.
I don’t think Chinese models care one iota about any of these advisory groups. Even if they’re one year behind the curve, a year or two is a piss drop in the grand scheme of things.
Who knows if they are behind or not?! Things like advanced math and advanced hacking require you to put a ton of effort into specifically training for those skills, and I've not seen any indication that the Chinese AI companies are interested in doing that - they seem more business focused.
I don’t know what’s wrong with Opus 5. I’ve been using Code since November 2025 and Opus 5 is the first blatant regression I’ve seen. Like you said, it just goes off into an endless loop doing random busy-work type of stuff. That’s the best way I can describe it. It’s doing stuff, but it seems mostly like busy-work to me. I’m not saying the model is “dumb” it’s most certainly capable, its vision is better than 4.8 but however they post-trained it is a fuckup.
Also whole heartedly agree with the Opus 5 output being incomprehensible. It’s written in a way that I’d call spaghetti-tech-English. You can unravel it but it’s painful. Fables explanations is effortless and smooth. Opus 5 is user hostile.
Are you familiar with the Thesaurus Linguae Graecae? It's a project that may meet your needs. Paywalled, unfortunately, but I assume it would be a one-time expense.
Two thoughts on someone who went out of their way to learn math:
1. If you can already program, the worst thing you can do is think of mathematics as learning a programming language. It is not, and you will waste your time being frustrated with things like syntax and notation. You get “used to” mathematics by doing it, and it’s something on its own. Just go with it. It’s ok to be confused.
2. Do the exercises, and stop asking for “solution manuals”, the point is to get you thinking and the struggle is most important part, not whether you got it “right”. Again, I think this is a programmer centric way of looking at things: “how do I know it’s
right if I can’t compile it”.
Maybe that’s why programmers like the foundations of mathematics. Like if somehow they could just go to the bottom of things, the assembler/machine code of sorts, the whole enterprise would make sense. Counterintuitively, the really great mathematicians of yore, did mathematics before it was anywhere close to formalized.
>Again, I think this is a programmer centric way of looking at things: “how do I know it’s right if I can’t compile it”.
I would argue this would only be true for those without formal education. Writing your code on paper is very common in CS courses. You get used to not being able to compile it.
I think your latter comment is kind of analogous to people writing python (or any high-level language) without understanding assembly. I think maybe that reduces the mystery a bit?
reply