You can't deny it if it's true, but the point is to find new techniques and abstractions. A proof you can't extrapolate and learn from is just a checkmark, and about as useful.
As far as I can tell from colleagues in other domains, it’s the same there. One paper will mention something off-hand and that’ll cause someone else to have a spark of insight, which turns into it’s own valuable research
Mathematics has to be also understood from the perspective of theory building, not just problem solving.
I couldn't disagree more.
A lot of mathematical "problems" are almost entirely pointless. Nobody genuinely cares about the moving sofa problem, or about square packing, or about the minimum number of colors needed to draw a map - it is the math that is developed during the solving process that is valuable!
An answer to a question like "what is the exact area of a unit circle" is a mere curiosity. Calculating a good-enough approximation is trivial, after all. But wanting an exact answer leads to developing calculus, which leads to most modern physics. Science was able to make a giant leap forwards due to the techniques developed, while the actual answer itself is mostly useless.
But let’s consider a hypothetical: what if an intuitive understanding of the true “boundaries” of mathematics (if such things exist) is beyond the capabilities of a human mind? If there truly is no way to simplify some proofs down from 200,000 line incomprehensible gibberish to something you could teach to a high schooler or undergraduate or even a PhD. Is the proof still worthless? Sure, at the moment, it might be. Finding such a proof and understanding the implications of it are different skills, the latter of which AI almost certainly does not possess at the moment. But there may come a time where the AI can view the bigger picture and make the leaps you described (say, an eka-Calculus from an eka-unit-circle). These leaps may be as unintelligible to us as the proof in OP is.
I guess the question is: assuming that we can’t make the proof beautiful enough to spark deeper human understanding, do we still want it if it sparks deeper AI understanding?
Personally I would hate to live in a universe where the boundaries of science are beyond intuitive human understanding, but I think it’s almost certainly the case. The idea that the rules are all within our grasp reeks of anthropocentrism to me. I would love for the universe to prove me wrong though. It’d be a pleasant, hilarious coincidence if they do fit within the boundaries of our understanding.
Mathematics and science are both about building structure on large classes of facts about the (logical or physical, respectively) universe that allow us to generalize our knowledge and make predictions about facts we cannot yet observe. This also lets us make claims about things that are, individually, too complex for the human mind to grasp, by abstracting away the complex details into a simpler structure and then making the claim about anything that satisfies that structure.
To put it another way, mathematics is about finding beauty — specifically those things that exhibit structure that humans can grasp. Modern mathematics, for the most part, makes no claims about what lies outside that space: if it turns out that the universe consists only of things that humans can describe through mathematics that would be neat, but in the much more likely case that it doesn't mathematics continues as it is today.
It's an interesting and maybe even useful trivium if (according to some set of axioms, such as those implemented by your favourite proof assistant) a fact is true, but it's not (human) mathematics, and if there's no useful way for humans to generalize from it there's no point in including it in a library of mathematics. It wouldn't be that surprising (but would be very interesting!) if there were an entire parallel class (or, more likely, family of classes, one for each AI architecture) of AI mathematics comprising structures that AIs can usefully generalize from. Such a thing has no reason to bear any resemblance to human mathematics, which is based on mapping structures to innate human linguistic and spatial intuitions, and may not yield any insights to human mathematicians.
By extension: why should we assume that a human would still understand the problems - or the answers? If all of it is complete gibberish to a human and can never be applied in any way, shape, or form, then what's the point?
The way I view it there are two options here: either you completely ignore it and end up burning a massive amount of electricity on what is essentially a bunch of LLMs jerking each other off, or you blindly follow it and end up with a Machine God who can justify a genocide with a "This is the correct thing to do. Trust me bro, I have irrefutable proof - you won't understand it". There's just no sensible way to do post-human math in an inherently human world.
"Okay, so what determines what is and is not allowed in the collection?"
"Whether the given substatement is true or not, of course."
Like this is obviously silly, right. In your view you could have two guys both trying to prove or disprove that the area of the unit circle is 3, and yet only the guy doing it with some vision of nobility where he's building up to this grand theory of approximations is the one actually doing "real" mathematics. The guy who's doing it just because he thinks it's neat and would like an answer to the problem itself doesn't count, and you suspect he couldn't even exist.
What did the alchemist truly learn from this interaction? Is the answer in any way helpful for him? Will it lead to him making gold, and the implied endless riches it entails? Why should it bring him him to ask follow-up questions with useful answers like "The technology to do this doesn't exist yet and can't be developed within several lifetimes" and "It'll never be economically profitable to turn lead into gold", instead of blindly being fed piecemeal steps in the impossible task of one medieval guy building a LHC?
Writing true statements is absolutely trivial, anyone can do that. There's an endless amount of true statement which have absolutely no value to humanity whatsoever. Their proof is meaningless without something to give it context. "Substatement 1304 is true" has significantly less value than "here's something I call 'group theory', and it might also be helpful solving open issues in fields X, Y, and Z".
Mathematics is about widening our collective understanding. There will of course be some people out there who'll hear "The answer to life, the universe, and everything is forty-two", think "Neato!", and go on with their day without giving it any further thought - but I'd have a hard time calling them mathematicians.
That doesn't mean it is completely useless, of course. A "prove that no efficient algorithm exists to break this new encryption scheme" would be very helpful indeed. Until you realize it neglected to take quantum computing into account, of course.
[0]: https://home.cern/alice-detects-conversion-lead-gold-lhc/
Now if you ask "does the area of unit circle equal 4?", I don't really know, but we can go back to the oracle and ask again (we haven't learned the general pattern).
Also, I'm not sure that assuming this 'area of circle' question was cutting edge math, that the oracle wouldn't say 'yes, to a certain level of tolerance'. Can't count how many times I've seen agent decide a test needs to be loosened or deleted because its an "edge case" or "blocking". If you don't understand the proof you might get back 'yes' for some versions of 'is the area of unit circle 3' (depending on complexity of that ask).
> Nobody genuinely cares about the moving sofa problem, or about square packing, or about the minimum number of colors needed to draw a map
I agree that solving problems along the way is incredibly useful too, but there's no math problem that I'm aware of that's utterly useless. Thing is, math is about abstraction and structure. You're developing tools. Those tools can be used for more than one thing. That's why math is often called a language. It's also why mathematicians and physicists end up being so helpful in other fields, because it was (most of them) about understanding the language of complex problem solving. Even code is math (I find it quite odd programmers are against math and elegance as these are directly in line with their goals, but I guess there's always a Dijkstra EWD already calling this out)
Where I fully agree with you is that solving hard problems advances us. TBH, it doesn't matter what it is. Fund NASA and you not only get men to the moon but velcro, GPS, and global wireless communication. Fund particle accelerators and you get the internet. Fund math and, like you said, you get a tool (calculus) which is worth more money than we can even imagine. The thing is that solving hard problems forces the unknown unknowns to become, at least known unknowns.
The beauty of the weapon IS the point. What it proves is derived from its use.