points by marhee 2 days ago | 0 comments
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?
[–] chr15m 2 days ago
Mathematics is machine verifiable, meaning you can automate RL at high volume.
[–] Kwpolska 2 days ago
Those proofs have not yet been verified by any human. It's quite likely those will turn out to be complete slop and gibberish on closer inspection.
[–] jen729w 2 days ago
> quite likely
Citation needed.
[–] suddenlybananas 2 days ago
A few have been retracted, although I agree the above comment is overstating how sloppy they are.
[–] roncesvalles 2 days ago
A lot of those proofs are slop and lack the elegance of a human solution.
[–] jen729w 2 days ago
A proof is a proof though. It's either true or it isn't.
[–] hxelk1 2 days ago
I only have a limited math background, but-
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.
[–] redf5 2 days ago
You are correct, but application of that knowledge might require understanding of why the proof is correct. Maybe not in all cases. The proof is the start of the process, not the whole thing.
[–] LtWorf 2 days ago
You can proof a lot of trivial things that nobody has bothered to proof. Then what?
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.