6 ms·

Terry Tao is a next level vibe coder: he inspires people to do his vibe coding for him. As someone with a background in advanced math, though never even close t

by norir 4mo ago

Terry Tao is a next level vibe coder: he inspires people to do his vibe coding for him. As someone with a background in advanced math, though never even close to Tao's level, I find myself skeptical about this type of mathematics. I don't personally find it beautiful and it feels like the line between the profound and the trivial (as in of minimal importance not difficulty) is blurry. One could argue for pure mathematics that is of no practical utility but is aesthetically beautiful, but I struggle to see the beauty in a gargantuan lean proof constructed by 100 different people. Perhaps this work will lead to deeper insight about the universe and the human condition, but I catch a whiff of problem solving for the sake of problem solving untethered from a deeper sense of purpose and meaning.

throwaway67678 4mo ago
Arguments about beauty don't lead anywhere constructive because they are too observer- and context-dependent. Poincaré himself was decrying continuous non-differentiable functions as abominations. The monster group is, well, just like that. What feels intellectually ugly for one generation is natural for the next, and the field moves on
- Ygg2 4mo ago
  According to legends Pythagoreans tried to surpress existence of irrational numbers because they couldn't be expressed as ratio of natural numbers Supposedly even drowned their member that divulged their existence.
- potbelly83 4mo ago
  That's not what op is arguing. To use your example, coming up with singular examples of continuous non-differentiable functions is an example of "ugly" mathematics, whereas putting them into a nice framework where they can be analyzed as a whole (i.e. functional analysis, density of such functions, etc...) is an example "elegant and insightful" mathematics. The same with the monster group, on its own maybe nothing special, but then you have the connections with other branches of math. Tao seems so focused on the individual problems and not their connections/generalizations.
  - throwaway67678 4mo ago
    Well one does have to come up with continuous non-differentiable functions to begin with, right? Weierstrass had to shock the community with his weird series that's almost everywhere nondifferentiable before people could conceive of a nice framework that includes them. People do not invent whole encompassing abstractions out of nowhere
    - potbelly83 4mo ago
      Great point, I think the argument you could make about Tao (fairly or unfairly) is he never tries to build that framework.
- threethirtytwo 4mo ago
  Agreed, mathematics is ugly without ai. I feel beauty is in massive complexity and intricacy. Every time I see a small proof it feels too easy and trivial. Triviality and simplicity is ugly to me.
- zerobees 4mo ago
  > Arguments about beauty don't lead anywhere constructive because they are too observer- and context-dependent. Meh. You can successfully argue that there is no objective anything. It's all just our perception and the emotions we associate with it. We built entire civilizations on subjective notions of good, evil, beauty, and so on. So where do you draw the line between "acceptably subjective" and "too subjective"? And are you sure it's not just a subjective code name for "the thing I don't like"? Ultimately, people practice mathematics mostly for abstract reasons. It's not a field where you routinely ship products and get rich by meeting market demand. If 99% of contemporary mathematicians don't want to become prompt engineers, there's nothing that makes the transition to AI math inevitable. If not mathematicians, the only party with vested interest in that would be the PR departments of frontier labs.
zem 4mo ago
the analogy with experimental physics is a good one - being sure something is true is a good first step to developing an elegant proof of its truth.
empath75 4mo ago
I think what people find beautiful in math is largely something that enables the mathematics (or physics) to be translated to something that they can think about intuitively, and what people can handle in an intuitive way is largely an artifact of what the brain evolved to be able to think about "naturally". But it's quite possible that most things that are true about the universe or math are just ugly and unintuitive, and the pursuit of truth shouldn't necessarily be limited by what people can easily reason about and hold in their heads. Beautiful explanations are lovely when they exist, but we shouldn't wait for them if we can also find the truth through an ugly method.
12345ieee 4mo ago
> 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.
- zerobees 4mo ago
  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.
  - setopt 4mo ago
    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?
    - jubilanti 4mo ago
      "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.
      - setopt 4mo ago
        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.
hashmap 4mo ago
> One could argue for pure mathematics that is of no practical utility wait what is the math with no utility
mswphd 4mo ago
the way to interpret the gigantic lean proof is not by inlining each lemma, looking at all the lines, and thinking "yeah that's a lot". That's also not the way to read a paper. Instead, you proceed in layers of abstraction. For example 1. the main claim may rest on some set of sub-claims, as well as some local (to teh main claim) work to "patch things together" 2. each of those sub-claims themselves may require other sub-claims + local work, etc These can be collected into a dependency graph. In lean, this is often called a "blueprint". Here is the blueprint for the formalization of the Polynomial Frieman-Rusza conjecture (now a theorem, by Gowers, Green, Manners, and Tao). https://teorth.github.io/pfr/blueprint/ https://teorth.github.io/pfr/blueprint/ This layer of abstractions is (roughly) equivalent a different way to format mathematics. You could remove the Lean component (let alone any AI), and create such a dependency graph for a paper. I would argue this is a clearer way to format mathematics (again, ignoring both the formal verification applications of it, as well as AI). Any mathematics paper intrinsically has a graph such as this underlying it, and tries to make the various linkages in the graph clear via prose. Prose is only so powerful a way to organize things. I'm sure you're familiar with the way early mathematicians would describe various formula (e.g. the quadratic formula) via prose. It is very hard to understand. Separately from this dependency-graph perspective, you can do things like 1. add formal verification. Now, each component in the dependency graph is verifiable with high confidence (though harder to write and read). This has some benefits and downsides. Harder to write and read is bad. Being able to have high confidence in the veracity of the result is *very* good. It allows larger collaborations in mathematics. Previously, a large collaboration would require all mathematicians to trust eachother to a large extent. This is (practically) difficult. 2. when each component can now be verified to high accuracy, you can now throw AI at it. I won't extoll the virtue of this. There are parts of it that seem interesting, but many "AI for Math" things currently are stil producing unformalized papers (in prose). Maybe the main thing I'd say is that this type of "graph structure, with each component trusted" is already implicitly what mathematicians do. You write papers that cite other papers etc. Except now, instead of needing to look for status signals to trust papers (or invest personal effort), you can look for another (honestly fairer) signal to trust papers. So there's a sense in which formalization allows for the democratization of mathematics. I do think there's something beautiful about that.

by norir 4mo ago

throwaway67678 4mo ago

Arguments about beauty don't lead anywhere constructive because they are too observer- and context-dependent. Poincaré himself was decrying continuous non-differentiable functions as abominations. The monster group is, well, just like that. What feels intellectually ugly for one generation is natural for the next, and the field moves on

Ygg2 4mo ago
According to legends Pythagoreans tried to surpress existence of irrational numbers because they couldn't be expressed as ratio of natural numbers Supposedly even drowned their member that divulged their existence.
potbelly83 4mo ago
That's not what op is arguing. To use your example, coming up with singular examples of continuous non-differentiable functions is an example of "ugly" mathematics, whereas putting them into a nice framework where they can be analyzed as a whole (i.e. functional analysis, density of such functions, etc...) is an example "elegant and insightful" mathematics. The same with the monster group, on its own maybe nothing special, but then you have the connections with other branches of math. Tao seems so focused on the individual problems and not their connections/generalizations.
- throwaway67678 4mo ago
  Well one does have to come up with continuous non-differentiable functions to begin with, right? Weierstrass had to shock the community with his weird series that's almost everywhere nondifferentiable before people could conceive of a nice framework that includes them. People do not invent whole encompassing abstractions out of nowhere
  - potbelly83 4mo ago
    Great point, I think the argument you could make about Tao (fairly or unfairly) is he never tries to build that framework.
threethirtytwo 4mo ago
Agreed, mathematics is ugly without ai. I feel beauty is in massive complexity and intricacy. Every time I see a small proof it feels too easy and trivial. Triviality and simplicity is ugly to me.
zerobees 4mo ago
> Arguments about beauty don't lead anywhere constructive because they are too observer- and context-dependent. Meh. You can successfully argue that there is no objective anything. It's all just our perception and the emotions we associate with it. We built entire civilizations on subjective notions of good, evil, beauty, and so on. So where do you draw the line between "acceptably subjective" and "too subjective"? And are you sure it's not just a subjective code name for "the thing I don't like"? Ultimately, people practice mathematics mostly for abstract reasons. It's not a field where you routinely ship products and get rich by meeting market demand. If 99% of contemporary mathematicians don't want to become prompt engineers, there's nothing that makes the transition to AI math inevitable. If not mathematicians, the only party with vested interest in that would be the PR departments of frontier labs.

zem 4mo ago

the analogy with experimental physics is a good one - being sure something is true is a good first step to developing an elegant proof of its truth.

empath75 4mo ago

I think what people find beautiful in math is largely something that enables the mathematics (or physics) to be translated to something that they can think about intuitively, and what people can handle in an intuitive way is largely an artifact of what the brain evolved to be able to think about "naturally". But it's quite possible that most things that are true about the universe or math are just ugly and unintuitive, and the pursuit of truth shouldn't necessarily be limited by what people can easily reason about and hold in their heads. Beautiful explanations are lovely when they exist, but we shouldn't wait for them if we can also find the truth through an ugly method.

12345ieee 4mo ago

> 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.

zerobees 4mo ago
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.
- setopt 4mo ago
  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?
  - jubilanti 4mo ago
    "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.
    - setopt 4mo ago
      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.

hashmap 4mo ago

> One could argue for pure mathematics that is of no practical utility wait what is the math with no utility

mswphd 4mo ago

the way to interpret the gigantic lean proof is not by inlining each lemma, looking at all the lines, and thinking "yeah that's a lot". That's also not the way to read a paper. Instead, you proceed in layers of abstraction. For example 1. the main claim may rest on some set of sub-claims, as well as some local (to teh main claim) work to "patch things together" 2. each of those sub-claims themselves may require other sub-claims + local work, etc These can be collected into a dependency graph. In lean, this is often called a "blueprint". Here is the blueprint for the formalization of the Polynomial Frieman-Rusza conjecture (now a theorem, by Gowers, Green, Manners, and Tao). https://teorth.github.io/pfr/blueprint/ https://teorth.github.io/pfr/blueprint/ This layer of abstractions is (roughly) equivalent a different way to format mathematics. You could remove the Lean component (let alone any AI), and create such a dependency graph for a paper. I would argue this is a clearer way to format mathematics (again, ignoring both the formal verification applications of it, as well as AI). Any mathematics paper intrinsically has a graph such as this underlying it, and tries to make the various linkages in the graph clear via prose. Prose is only so powerful a way to organize things. I'm sure you're familiar with the way early mathematicians would describe various formula (e.g. the quadratic formula) via prose. It is very hard to understand. Separately from this dependency-graph perspective, you can do things like 1. add formal verification. Now, each component in the dependency graph is verifiable with high confidence (though harder to write and read). This has some benefits and downsides. Harder to write and read is bad. Being able to have high confidence in the veracity of the result is *very* good. It allows larger collaborations in mathematics. Previously, a large collaboration would require all mathematicians to trust eachother to a large extent. This is (practically) difficult. 2. when each component can now be verified to high accuracy, you can now throw AI at it. I won't extoll the virtue of this. There are parts of it that seem interesting, but many "AI for Math" things currently are stil producing unformalized papers (in prose). Maybe the main thing I'd say is that this type of "graph structure, with each component trusted" is already implicitly what mathematicians do. You write papers that cite other papers etc. Except now, instead of needing to look for status signals to trust papers (or invest personal effort), you can look for another (honestly fairer) signal to trust papers. So there's a sense in which formalization allows for the democratization of mathematics. I do think there's something beautiful about that.