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.
An inscrutable 1000-page Lean proof may have low transmissibility amongst humans, yet extremely high transmissibility amongst AI mathematicians.
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.
Mathematics is a language for humans, not just for machines. We may agree to let machines "do their thing" for as long as they want but to what purpose? Just creating "results"? What is a mathematical result by itself?
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.
I'm not sure why we would assume that AI-generated or AI-assisted mathematics would never amount to anything useful in the real world. I would expect the opposite: the usefulness and explanatory power of mathematics has been riding an exponential over the last several centuries.
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).
> a 1000-page proof with no possibility of transmission
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.
"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.
When writing code I also believed in the "beauty" and "elegance" because IMO it opens up all kinds of different opportunities that involve using or organically growing or improving that code. It turns out that if it doesn't solve a quantifiable problem, (mostly) nobody cares. And the pace of innovating in the field outgrows the pace (by a large) of keeping things "beautiful and elegant".
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.
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.
That is perhaps fair, is that distinction common internationally?
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.
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.
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.
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.
"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)?
The vast majority of research-level pure mathematics is never going to get used in science or engineering. Obviously it is hard to predict what will be useful, but for the type of mathematics that is unlikely to be, there is a question as to why we care about it, and that almost has to come down to beauty in some sense - some mathematics gives us a new lens to look at parts of the mathematical world and others chip away at problems in more mundane ways in the hope that they inspire or contribute to new parts of mathematics that are beautiful.
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.
I don't know how you think it only gives you Lean - it gives you everything including the explanation. You can actually ask it explanation using you know.. natural language.
> 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!
Oh no, imagine the people that save human lives having high salaries, the horror.
If you, like me, are in the software field, know that this is likely the most comfortable job even invented by humanity, we should really be paid just above the poverty line in exchange.
However many others in society save lives that are not so lavishly praised or financially rewarded.
For example in New Zealand median pay for a Road Design Engineer is about $100k NZD compared to a GP (doctor) getting $240k. Plus the doctor gets paid a massive overpayment of social status.
Over a 40-year career, an average NZ GP will save 5 to 10 lives. The Road Design Engineer saves 40 to 120 lives. Road engineers in NZ prevent roughly 10x more serious injuries than they do deaths so it isn't just death stats.
Our hypothetical engineer should be paid > 10x more than the doctor on raw stats.
It gets harder when we start looking at quality of life versus raw lifetime numbers. You then need to consider the value of say entertainment (a good movie) versus the hypothtical lives saved by spending the budget elsewhere.
A game designer might be valued highly by a gamer mum, and negatively by their children and gaming widowed dad.
Give me a break, most of them are glorified drug dealers. Their salaries are inflated by an artificially capped supply of doctors, at the cost of patients.
I had to leave my job this year because of burnout when the execs mandated that we use AI tools, become our own designers, PMs, and QA, and double our velocity. They run through a decision tree they leaned in residency every day and I’m learning how to do 3-4 other people’s jobs on top of whatever the new AI thing is. I was working nights and weekends while my friends in medicine are planning their 3rd vacation this year to Tuscany.
The early theorists of capitalism didn't imagine that advanced psychology (that didn't even exist back then) would be used to convince people to buy $product.
Messages of that sophistication are always dangerous, and modern advertising is the most widespread example of it.
The hostility is more than justified, I can only hope the whole industry is regulated downwards, even if whatever company I work for sells less.
Not to mention their pro features keep breaking syntax of the community version, obviously with 0 transparency.
Now, of course they should get paid for the work they do, but these sort of "we were FOSS and surprise we're not anymore" are becoming commonplace and are always done hoping no one notices.
Honestly, FSL doesn't break any flow for day to day developers. What's the harm? I am curious to know. On the contrary I like competitive vs non-competitive distinction.
Most of us don't want to let a court decide if we compete with a very general distinction you describe, and can't afford lawyers to evaluate a 2 year old license without much case law.
Most of us prefer not to bring on a dependency in our project that is primarily designed to extract commercial value from users and is less friendly to contributors than similar open source projects.
It’s because big tech companies have spent millions to foster goodwill towards the OSI Open Source definition. And there’s a general feeling that software that fits that definition is pure and any that doesn’t is unclean.
Just to be devil's advocate here, and pedantically point out that Debian Sid is not a "distro", I don't think it's correct to say that Debian unstable is "actually stable", because it's "unstable" from the perspective of Debian, not from a subjective, individual experience.
Debian release cycles have a strong focus on stability, and for those situations where it matters, like running a production server, that is a pretty important feature. Just because your desktop never broke doesn't mean it's not "unstable", it's more of a disclaimer that if you put serious things on top of it and it breaks, that's much more on you because you chose to go against maintainer advice.
For me personally, with exception of the Enterprise Linux family (Alma, Rocky etc.), there's no Linux distribution I'd rather run on a workhorse, production, long term deployment server than Debian.
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.
reply