Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- 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.by norir
- > One could argue for pure mathematics that is of no practical utility
wait what is the math with no utility
by hashmap - 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/
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 mswphd - 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.by zem
- 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.
by empath75 - 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
- > 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.
by 12345ieee - I think Terry Tao is a great litmus test for AI zealotry (both pro- and anti-). Just in this thread, we have people twisting themselves into knots about how he "sold out" or "not doing math the right way" or whatever. To him, AI is a tool, like any other.
From the interviews I've seen with Tao, he's not some AGI maniac, he says things like here's where we can use this tool, here's where it's less likely to be useful. There's a lot of hallucinations, so we need to double check stuff. Most of the stuff the AI produces is nonsense, but there's occasionally a diamond in the rough.
A very tempered attitude, and likely what most sane people are experiencing when using AI.
by dvt - > I think Terry Tao is a great litmus test for AI zealotry (both pro- and anti-). Just in this thread, we have people twisting themselves into knots about how he "sold out" or "not doing math the right way" or whatever. To him, AI is a tool, like any other.
That’s an Anti example. What’s a Pro example?
by keybored - A smart phone was just a tool at first, but over time society has become overly depedent on them. Most of us are now addicted to our smart phones in one way or another, and that has consequences that play out across society as a whole.
AI not only provides potential to cause society to become overly dependent on it, but it's being developed by/pushed for by the same fucking people who caused our societies smartphone addiction.
Once you recognize what we've lost already, it's hard to turn off your brain and just compartmentalize this away as a "just a tool". Nothing that is adopted so widely is "just a tool," and thinking of it in those terms eliminates the ability to analyze the potential downstream effects it will cause.
by jplusequalt - I enjoyed the article. I'm not a mathematician, but I did notice one aspect: even with his enthusiasm for AI, Tao effectively showed that for the uses he describes, AI can currently only handle small chunks of a mathematical problem at a time. Humans, or non-LLM approaches are still needed to stitch these together.
It perhaps isn't too different from LLMs being able to coherently output short, a few hundred words, pieces of prose, or code, but not being able to assemble them into functional output with constant "nudging".
Happy to be corrected on this!
by pcrh - If good mathematicians are able to design ML recipes for maths (may be field specific), using maths solvers, I wonder what will be the size of their proofs...
All that to find a path to true or false.
by sylware - mathlib and lean are currently too cumbersome for many researchers to use in say algebraic geometry, but maybe more suitable for combinatorics where it has been applied recently.by vitriol83
- I have a tangent question: is there a formal language definition of mathematical grammar the same way there is for a programming language? If so, is it context sensitive or context free?
I was daydreaming about how someone would model symbolic algebra in computer code, and naively thought it would be easy, but the more I thought about it, it seems to get exponentially (pun intended) more complicated.
by gosub100 - Yes, people are using the programming language Lean for that, and there are a few less popular alternatives as well.
Fundamentally, there is a one-to-one correspondence between mathematical proofs and programming. Proofs are isomorphic to type checking.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
by 317070 - the smartest people see AI as an incredible tool that enhances their productivity.by ruilov
- There is more to life than productivity.by Jtarii
- The smartest people *usually* have little idea how *us* mortals can abuse the GenAI tools, because they are aware of their limitations, but we aint.by bawis
- You went so deep there champby witx
- Just like me! I like AI because of how smart I am.by big-chungus4
- I should really know better than to say something like that for a figure as revered as Terry Tao, but, he has taken OpenAI's money to shoot an advert for them [1] and, sorry but I can't believe he is entirely unbiased; or very unbiased for that.
_____________________
- Do you have any evidence that he took their money?by lupire
- "Tao has sold out to the AI grifters to prop up the AI hype bubble" is not a take I expected to see.
I think we can all be a bit grounded and understand reality as we see it -- one of the smartest living mathematicians is using an important invention. Not necessary to believe in any conspiracy theory.
by simianwords - I do not know about this but, to be honest, he (or his Dpt, or whatever) has the money and connections to try the hidden-behind-closed-doors stuff.
We mere mortals (I am a prof. of Maths at Uni) do not.
by pfortuny - I think it helps his credibility that he has been working with and speaking positively about AI assisted mathematics (especially for formalizing proofs) for over a year now . I'm sure he isn't unbiased, but as far as spokespeople in the AI space are concerned I'd count him among the less biased ones.by fxwin
- More accurate title would be "Terry Tao Became an Evangelist for Lean"by nylonstrung
- I really look forward to the day AI-driven algorithm design + formal verification becomes the norm for performance critical computing.
A programmer translates a natural-language spec into a machine-readable spec, feeds it to an AI-assisted compiler, and out pops an implementation that's more optimized than any human could ever hope to write, along with a lean proof of its correctness.
by pvillano - ...and no human will be able to understand the algorithm either.by xg15
- I'm sure a system that could do this is economically optimal.
Why are you looking forward to this, though?
by xpct - > A programmer translates a natural-language spec into a machine-readable spec
Why do we need a human for this?
by dyauspitr