> 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.
> 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.
Much (most?) of math consists in transmission of it (according to Thurston [1]), a 1000-page proof with no possibility of transmission is mostly useless. The proof of Fermat's last Theorem is important in itself, and adds much more than the mere result.
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...
What is the difference between "beauty" and "elegance" of a proof?
"Beauty" is something I cannot define. "Elegance", as I use it, is the use of tools as precisely as possible. It is a technical term, whereas "beauty" I cannot define.
Of course, that is my view of it.
You are mixing a lot of categories here -- beauty, verbosity, utility, elegance, insights.
Why all that when you just need one thing: truth.
> Why does it need to be beautiful?
"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)?
Outside of some niche specializations like cryptography, math isn't practiced because of "consequences". Most mathematicians take pride in their work not having any obvious practical applications. They're also overwhelmingly working in university settings where they're not expected to generate revenue or deliver practical results.
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.
Most mathematicians don't take pride in their results having no applications. That's just not true. Maybe some quirky pure logicians or something. But otherwise 90%+* of mathematicians I know would be at least satisfied if not thrilled for their work to be used by others.
*Completely made up statistic.
You put it perfectly. And all these AI math startups don't actually care about mathematics. They are just using it as a proxy for general reasoning, with the VC pitch being some kind of world domination after they crack these problems.
Are you sure that’s «most» mathematicians?
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?
"Applied Math" and "Statistics" are distinct fields from "Mathematics," not subfields of it. People in those two departments are often closer to Computer Science or the statistics subfield in a domain science field (e.g. biostatistics, econometrics) than to Mathematics in terms of what they actually teach and research.
You want to understand why it’s true, and that often correlates with beauty.
How is this relevant here? AI helps you understand the why -- it literally discovers the proof and hands it to you with explanations. It hands you the proof that you would have otherwise not found easily.
If the proof is hundreds or thousands of lines of Lean, it’s not clear that the AI will be able to provide an insightful “why”, instead of just dozens of microsteps.
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.
Why prove the Pythagorean theorem rather than just prove 3^2 + 4^2 = 5^2?
For any practical application, you are only interested in finite set of concrete identities, so anything beyond that is surplus to requirements, surely?
I think you may be interested in more abstract things. In this case, let's say you're creating a program for a 3D printed thing, and you have to fit a diagonal cardboard in a rectangular box, you'd like to be sure that the Pythagorean theorem holds even in cases where you haven't tried it out.
> For any practical application, you are only interested in finite set of concrete identities
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.
The current commentators are surely missing the fact that this comment is sarcastic.
You meant this as satire, right?
> Why does it need to be beautiful?
“Beauty will save the world”