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?

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.

> quite likely

Citation needed.

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

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 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.

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

Out of curiosity, is Joel Spolsky still involved in SO? What’s he up to these days?

I enjoyed reading his articles but it feels eons ago.

He's gone, probably fully retired. He doesn't even attend conferences anymore.

I sort of feel the same. I also don't understand why - it seems quite natural to make it smaller and cool and they for example release new level packs, maybe free even (or for a small price). I've also never understood why he didn't make a sequel for Braid. Such a cool game. You're not milking it if you make a sequel it deserves.

> I've also never understood why he didn't make a sequel for Braid. Such a cool game.

Perhaps it's such a cool game because it doesn't need milking or sequels? Perhaps he never made a sequel because he doesn't want to repeat the same things ad infinitum?

FUD used to pump value