How does this comment fare with the recent drop of 700 or so novel math proofs? Is math intelligence possibly the outlier because math is the most self-contained knowledge where absolute truth is the easiest to establish?
It seems like LLMs are just guiding an extreme brute-force search (there's a reason they didn't use a single Astra agent, but 10s of thousands).
I'm curious if there are maybe a few million mathematical statements, and only a certain subset will connect at the search nodes you're on. If we had such a DB (which is currently the LLM), how effective such a search would be? This is a bit like program induction but on a math theory. Perhaps the limit so far has been lack of such a database, no one has put every math paper into a formal LEAN proof so it can be leveraged.
A lot of key breakthroughs so far seem to just be "recombination" of existing things (not a massive quantum leap in new math), so perhaps we just need to automate this via search (and not with a very expensive intermediate database of LLMs).
Of course, I've read that just compiling the core math lib of LEAN takes 10+ minutes, so its not exactly a fast process at the moment, so quality of guess is probably a limiting factor.
Citation needed.
You're only looking at the symbolic part: deriving a statement from prior statements. I agree that the derivation either is correct or isn't.
But then there's the rest: the philosophy and intuition behind the symbolic manipulation. You can skip that if your goal is to use the results, but I don't think you can skip that if your goal is to develop the field.
I feel great sympathy for the mathematicians. This must be gut wrenching. It will lead to progress eventually, for sure, but right now a lot of them are in a bad place.
Edit: for readability.