My intuition is the opposite? The math results we are seeing lately are done with theorem provers. LLMs are getting very good at this and surpassing what humans have been able to prove. Verified code is traditionally very expensive and only applicable in niche areas when done by humans.
> LLMs are getting very good at this and surpassing what humans have been able to prove.
But if the reverse were true it would be impossible to prove. AI is trained on all of humanities solutions - LLMs stand on the shoulders of giants, not the other way around.
As of today, the training data the originates from humans represents a vanishingly small portion of the total training. The vast majority of training - how many 9’s is a trade secret - of a frontier model is synthetic RLVR data. That’s how they got good at this.
I thought only like a third (maybe 2/3?) of the training was RLVR?
We do, too, as we have also been trained from the same prior solutions.