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.

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

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.

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