A lot of those proofs are slop and lack the elegance of a human solution.

A proof is a proof though. It's either true or it isn't.

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.

I wasn't making a value judgement. I was being scientific.

You can proof a lot of trivial things that nobody has bothered to proof. Then what?

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.

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.

> quite likely

Citation needed.

A few have been retracted, although I agree the above comment is overstating how sloppy they are.

Mathematics is machine verifiable, meaning you can automate RL at high volume.

I wonder, now that we see how far "dumb" approaches to math have gotten, if we just had a massive DB of every math statement that has been proven so far, and we had a program that had 10s of thousands of GPUs running vectorized proof solvers, and we just started doing a search from the final proof statement to underlying axioms, how far we would get...

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.