> I struggle to see the beauty in a gargantuan lean proof constructed by 100 different people
Why does it need to be beautiful? Once you proved it it's true and you can use its consequences in math, sciences and engineerings.
Why does it need to be beautiful? Once you proved it it's true and you can use its consequences in math, sciences and engineerings.
I am not talking about the supposed "beauty" of a proof (I do not believe in that concept, rather in "elegance", which is not the same), I am talking about the proof itself, and the insights it provides.
[1] https://www.ams.org/journals/bull/1994-30-02/S0273-0979-1994...
Of course, that is my view of it.
Why all that when you just need one thing: truth.
Probably AI mathematics needs a specially constructed or trained translation or compression system (likely also an AI system) that helps transmit dense Lean proofs back into human-style thinking. We may even see an entire field develop around creating human-comprehensible compressions of vast formal breakthroughs in mathematics. Such an activity would almost certainly be both art and science -- there's some objectivity in that certain abstractions or definitions inherently cover more ground more efficiently, yet there's also a deep creativity and artistry in finding compressions that are adapted to the specific 3+1D spatiotemporal intuition of the human mind. Perhaps with time this will keep a lot of the originality and creativity of research mathematics alive -- maybe with that work having even more centrality than it does today.
Instead of seeing this all as a loss of beauty in mathematics, I choose to see it as the beginning of a new age, which will bring entirely new problems to solve, yet also accelerate discovery at an exponential rate.
Unless, of course, we are willing to give machines the responsibility of building bridges. Subject on which I do not have a clear opinion yet.
But just hard drives (or whatever) filled with bytes representing strings representing nothing any human will ever understand... I am not for it (as of now). There are much more important problems to solve.
Maybe I didn't do a good job explaining it, but the rest of my prior comment was about connecting AI-generated results back into human-style thinking. Inevitably, in the far future, it's not unreasonable to assume the world will be dominated by synthetic robots controlled by artificial intelligence, and there will indeed be a point where AI builds not just bridges but vast planetary, interplanetary, and space-based infrastructure projects beyond the ability of our current civilization. At that point, mathematics may permanently move beyond the grasp of the human species. You can't teach a dog general relativity. Surely, there are truths in mathematics (and possibly physics) you cannot teach a human. Not to digress, but for me, this kind of threshold is what a term like "superintelligence" means -- the point where an intelligence is discovering truths that cannot be taught back to humans because we're not smart enough. So far, our contact with this kind of intelligence has been limited to one-off, highly specialized cases (like chess) that have little grand implication for civilization, but that won't always be the case.
But, for today and probably at least our lifetime, to make them useful major AI advances in math will need to be "compressed" back into the specific network and "towers" of concepts and abstractions that human minds specifically can understand and intuit about. So I think both directions of formalization are equally important: translating natural language statements (theorems, lemmas, etc.) faithfully into Lean and letting a theorem prover run and decoding a dense Lean proof back into natural language (which, in some ways, is the more creative and open-ended problem -- there is no one right answer).
Have you actually looked at LEAN proofs? They are typically split into small bite size definitions and proofs, making it easy to dive in where you want, and skip what you don't care about, while knowing that you can trust the conclusions.
I personally think that having hundreds of mathematicians working together as a team is a beautiful thing.
We basically subsidize the practice of mathematics as an art form, and if you try to take the artistry away, you might find that the artists don't want to play along. And I guess you can imagine future robo-math production lines without any human involvement, and then LLMs finding applications for the resulting theorems, but it's not possible today.
At the universities I’ve been to (as a student and now faculty), «applied mathematics» and «statistics» have been the two largest divisions. But perhaps that’s a bias from engineering-heavy universities?
Again, in the universities I’ve been to, «applied math» and «statistics» have generally been placed under the department of mathematics. I myself am a physicist, and consider applied physics, biophysics, etc. to be subfields of physics and not distinct fields of study, but I don’t know what outer physicists think.
*Completely made up statistic.
For any practical application, you are only interested in finite set of concrete identities, so anything beyond that is surplus to requirements, surely?
I do a lot of numerical work in settings where computational efficiency is useful.
In my work, most cases you can do numerically using integration or Monte Carlo sampling or whatever.
It’s slow. It often pays to find a closed-form solution. Even if it’s just a starting point that needs refinement.
To put in terms of the Pythagorean theorem: Proving the Pythagorean theorem gives you a relationship that’s reliable, fast to evaluate, and general. Proving individual tuples gives you none of this.
That doesn’t even touch on how theorems give us a glimpse at deeper structure and truths. Proving a bunch of right-triangle tuples will probably never lead you to the rest of the identities in trig.
"Beauty", IMO, signifies the idea that you're doing `something` for its own the sake where "its own sake" approximate the idea of getting/being closer to (or in proximity of) `something`/`anything`/`someone` you find "beautiful".
> Once you proved it it's true and you can use its consequences in math, sciences and engineerings (sic).
The expression "you can use its consequences in ..." suggests that the action is a "just a means" to "something else". However, not everyone is interested in the idea of "something else"; they're interested in the idea itself (in a broad sense) as that's one of the main reason they got started/involved in the first place.
---
We all do things as "just a means" to "something else". However, there must be an "end" to this chain of "something else"; otherwise, how do you find any "meaning" (or sense of fulfillment) in this whole enterprise (or chain of "something else"s)?
And if it can provide insightful “whys”, that still correlates with beauty then.
Given the slop-like nature of what current generative AI tends to produce, I wouldn’t however count on the latter quite yet.
> And if it can provide insightful “whys”, that still correlates with beauty then.
Yeah it can, you just have to ask it. It has a good interface for it - text! I think you misunderstand how this tech works, its not just spitting out things. It has the understanding also and you can verify it by asking!
“Beauty will save the world”