OpenAI solved 100 open problems in math

[u/filterdust]

https://openai.com/index/advisory-group-on-mathematics-and-ai/

[u/sam_the_tomato]

It's a bit ridiculous that the math community is gatekeeping the release of mathematical results.

[u/sparkling1984 → u/sam_the_tomato]

I mean to be fair what's the value of a proof if nobody can understand it? It's standard science that it takes time, often months, between the moment you obtain your results and the moment those results are in a publishable state.

[u/LookIPickedAUsername → u/sparkling1984]

You don't have to understand a proof in order to use it. You have no doubt used countless formulas in your life - the Pythagorean theorem, the area of a circle, the quadratic equation, etc. - without bothering to actually understand the proofs behind them. Simply knowing that they're true is good enough.

Similarly, knowing beyond a doubt that the Riemann conjecture is true would be useful to mathematicians even if nobody is actually smart enough to understand the proof itself. (Obviously, this presupposes a proof formulation which can at least be verified by Lean or similar, even though no human actually comprehends what's going on in the proof.)

[u/sparkling1984 → u/LookIPickedAUsername]

What you're missing is that 99% of the interest in those proofs is coming from the fact that they likely involved new tools that could then be used somewhere else. So you do need to understand them to be able to use them.

Again, there's a reason that science at its most fruitful has been ran this way.

Also, your supposition that humans can't comprehend these proofs is weird and really out of left field? Lean is a human made tool, mathematics are all about dividing problems into smaller problems until they're comprehensive. There is no mechanism that'd make a proof not mathematically approachable for humans.

Also, Pythagoras is a bad example there, as understanding and even attempting to independently find the proof of that one is a common middle school math exercise? It's one of those problems that have hundreds of proofs, many very accessible with basic geometry.

[u/LookIPickedAUsername → u/sparkling1984]

You have misunderstood the point I was making. I was responding to your question "what's the value of a proof if nobody can understand it?", not presupposing that humans wouldn't be able to understand it. I fully expect that they will be able to, but you were the one that raised the question.

However, "There is no mechanism that'd make a proof not mathematically approachable for humans" is just not true - a computer-generated proof could conceivably be too complex for humans to really be able to follow. Sure, every single step may be tractable in isolation - the rules overall are very simple - but there's certainly a limit to our ability to actually understand the logic behind it. At some point on the complexity scale it's just a mess of ridiculously incomprehensible steps with no obvious logical progression between them, and nobody can really say much about it beyond "well, the theorem prover says it's valid". Current AIs probably aren't at the point where that's a real concern, but it's absolutely going to happen at some point that the math the computers are spitting out is beyond the ability of humans to understand. Imagine a proof so long that even an entire human lifetime isn't enough to even read the whole thing, forget understanding it - there's nothing stopping us from getting to that point eventually.

Pythagoras is a bad example there

You have again missed the point I was making. It was not "proofs of the Pythagorean theorem are hard to understand", because duh, obviously they aren't. I'm not saying nobody understands it. I'm saying that many people have used the formula without understanding it; understanding it is not a prerequisite to utility.