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.

Citation needed.

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.

I have a gut feeling this is the last juice because for 2 years now they have been "beating benchmarks" yet relatively simple tasks they still can't do sometimes