7 ms·

How Terry Tao became an evangelist for AI in math

192 points by Tomte 4mo ago

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.
nylonstrung 4mo ago
More accurate title would be "Terry Tao Became an Evangelist for Lean"
vitriol83 4mo ago
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.
ruilov 4mo ago
the smartest people see AI as an incredible tool that enhances their productivity.
- big-chungus4 4mo ago
  Just like me! I like AI because of how smart I am.
  - bigfishrunning 4mo ago
    I'm suddenly missing the slashdot mod system. +5 funny.
- llamacld 4mo ago
  [dead]
- Jtarii 4mo ago
  There is more to life than productivity.
  - fasterik 4mo ago
    Productivity is relative to whatever we value. That could be building things, making art, making scientific discoveries, or delivering food to people in poverty. Maybe you value non-tangible, non-durable things like experiences. That's great, but it would be weird to tell someone who's devoted their life to X "there's more to life than X." (Replace X with any of the fields mentioned above.)
    - brookst 4mo ago
      And experiences absolutely benefit from productivity improvements. AI has helped me plan better trips, find places and activities I had no idea about, better prepare for weather in remote destinations. It’s said that “productivity” is mistakenly connoted as scoped to work.
    - Jtarii 4mo ago
klmarks 4mo ago
Quantamagazine is essentially Renaissance Fund, which is heavily invested in AI. This is a clever piece reminding people of Tao's pre-AI Lean efforts. Now, however, Tao and especially Gowers are receiving AI money and have AI positions so they are far from unbiased. Or maybe they have caught Feynman's "computer disease"? Either way, this is a hype piece.
- TimorousBestie 4mo ago
  Tao doesn’t seem to have been all that corrupted by the AI money. He’s signatory to the Leiden Declaration after all.
  - bmitc 4mo ago
    Doesn't that require you to just click a few buttons? It's not like it's a binding pledge.
- YeGoblynQueenne 4mo ago
  Ahem. Define "Pre-AI". Automated theorem proving has been an AI task right from the very beginning with Simon and Newell's Logic Theorist, presented at the Dartmouth workshop in 1956. Logic Theorist soon proved 38 of the first 52 theorems in chapter 2 of the Principia Mathematica. The proof of theorem 2.85 was actually more elegant than the proof produced laboriously by hand by Russell and Whitehead (2026-03-20: What is called here Theorem 2.85 is, in fact, numbered as 2.53 in the page 107 of the 1963 Cambridge University Press edition (https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_Mathematica_vol1.pdf https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_M...) and which appears, under the same 2.53 number, on page 112 of the 1910 CUP Edition, according to the digitalization on wikibooks (https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Principia_Mathematica/Part_1/Section_A#Discussion_2 https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Pri...)). Simon was able to show the new proof to Russell himself who "responded with delight".[17] They attempted to publish the new proof in The Journal of Symbolic Logic, but it was rejected on the grounds that a new proof of an elementary mathematical theorem was not notable, apparently overlooking the fact that one of the authors was a computer program.[18][17] https://en.wikipedia.org/wiki/Logic_Theorist#History https://en.wikipedia.org/wiki/Logic_Theorist#History Maybe some people only understand "AI" to mean "LLMs" but, particularly in maths, LLMs ain't going nowhere without a symbolic solver (or a human mathematician) verifying their output.
cryo32 4mo ago
And I thought it was cocaine.
YeGoblynQueenne 4mo ago
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. _____________________ [1] https://youtu.be/cdflu9ZXZGE?si=f1xi65r7kZM8s1JI https://youtu.be/cdflu9ZXZGE?si=f1xi65r7kZM8s1JI
- pfortuny 4mo ago
  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.
  - fn-mote 4mo ago
    I won’t downvote this thread but … the first paragraph of the article explains how Tao won some $3m award. Unless the going rate for AI-shilling is much higher than I can believe, the amount of money just is not going to be enough to get a world-class figure to suddenly sell out. If you saw him selling his morals regularly in the past, ok I’ll listen to the evidence. But suddenly now? After so long writing (essentially for free) and building community? Doesn’t make sense.
    - fragmede 4mo ago
      A $100,000 investment into Anthropic or OpenAI a few years ago would be worth a couple hundred million today, so $3m is ~nothing in that scheme of things.
    - nilkn 4mo ago
      I don't think Terence Tao sold out. However, just looking at it from OpenAI's perspective, this kind of advertising is almost certainly worth at least one order of magnitude more than $3M to the company.
      - Quarrel 4mo ago
brcmthrowaway 4mo ago
It seems Cameron Zwarich has also joined OpenAI Is there a Lean/OpenAI connection?
- saagarjha 4mo ago
  Where did you see that?
gosub100 4mo ago
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.
- 317070 4mo ago
  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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
  - gosub100 4mo ago
    Thank you for this.
pvillano 4mo ago
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.
- jplusequalt 4mo ago
  >A programmer It won't be a programmer doing this work, because they will have gone the way of the dodo. It'll be workers specific to a certain domain (e.g. engineer, architect, accountant) doing this on top of their usual work. The software industry will collapse.
  - CuriouslyC 4mo ago
    The architect/accountant won't be doing it either, they'll just be a liability lightning rod for people who are closer to devs than architects doing the actual day to day work. Sort of like a doctor will "manage" a team of nurse practitioners.
    - whattheheckheck 4mo ago
      Except medicine is 1000x older than software engineering as a field
- xpct 4mo ago
  I'm sure a system that could do this is economically optimal. Why are you looking forward to this, though?
  - AndrewKemendo 4mo ago
    Not the OP but for me it’s: more optimized than any human could ever hope to write, along with a lean proof of its correctness.
- 4mo ago
dvt 4mo ago
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.
- jplusequalt 4mo ago
  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.
  - dvt 4mo ago
    > pushed for by the same fucking people who caused our societies smartphone addiction Not sure where you live, but I would guess the West (where we have the luxury to be worried about "smartphone addiction"). I assure you that the net positive of smartphones, especially cheap Androids, have had a significantly more positive effect on society than negative, particularly in the developing world.
    - jplusequalt 4mo ago
      >But I assure you that the net positive of smartphones, especially cheap Androids, have had a significantly more positive effect on society than negative, particularly in the developing world. My point is that the tool which was meant to augment one particular aspect of life, has metastasized into being a cancer on many other aspects of our lives, and that has downstream consequences on society as a whole. Keeping this in mind, being a bullish on AI seems foolish. edit: Perhaps a better thesis for my reservations with rapid technological progress: smart phones were supposed to help us adjust to society, but society instead adjusted to them. AI is positioned to do the same, and we need to ask ourselves what those changes could look like, and if they're for the better, or for the worse. >where we have the luxury to be worried about "smartphone addiction" I reject this, and any similar framing that amounts to "because there are other, greater problems at play, worrying about this relatively lesser problem is worthless." A problem that impacts people is a problem that deserves attention, especially if an absolute terms the number of people impacted are in the tens/hundreds of millions.
arjie 4mo ago
Woah, guys, the article is actually super cool. I almost didn't read the article because of the AI thing - I follow him on the microblog networks and I know he's pretty good at using LLMs and so on so that's not interesting. The unique stuff about him and gowers that it points out is there idea for massively parallelizable mathematics problem solving. It's definitely worth a read for how they got the first Polymath publication and afterwards for how they want to use LLMs et al. to do this: > He predicted that in the future, instead of working alone or in small teams of two or three, mathematicians might work on projects with hundreds of other people at a time. And when these collaborations were over, he said — in his modest, understated way — the results might be checked not by human referees but by computers. Fascinating stuff. My thought has always been that the AI will accelerate individuals and we'll get something like the economy for music or sports (the top few take almost all the revenue) but this may seem like an alternative pathway that might well develop (if only in Mathematics there) where AI systems drop the coordination cost to near zero by making checking cheap. So far, and I am not foolish enough to say forever, agents are great at operating in the space of checkables and it's hard to get uniqueness out of them (I haven't succeeded in getting a real laugh from Fable) but perhaps there's a whole class of problems that we can now solve by turning humans into the search units. I love it!
- InkCanon 4mo ago
  The checking has nothing to do with AI, despite the (massively funded) marketing done to make you think so. It is based on formal methods/theorem provers.
  - dellamonica 4mo ago
    The point of the AI with respect to checking is to translate a natural language theorem and its proof into the formal system. Most of known math is not formalized because it is very hard to do so.
  - world2vec 4mo ago
    From what I've seen on Tao's YouTube channel, he does use GitHub Copilot via VSCode to write Lean4 code.
bsoles 4mo ago
As much as I like Terrence Tao, I think he is entering the crackpot phase of his career. Much like Roger Penrose and many mathematicians and physicists before him.
- rowanG077 4mo ago
  Wild take, without even substantiating it with a single statement.
- justanotherjoe 4mo ago
  Yeah mathematicians tend to do that. Physicists not so much I think. However, none of what he says about AI is such a strong prediction, unlike the 'crackpots' that are probably on your mind.
  - limflick 4mo ago
    That's what all the Physicists tell me.
  - cryo32 4mo ago
    As a mathematician who was married to a physicist, I disagree :)
- gameshot911 4mo ago
  And maybe we should listen to him...
spondyl 4mo ago
I guess fandom is just in Terry's DNA: http://shanghikid.50megs.com/Otakudom/ContReal/contReal.htm http://shanghikid.50megs.com/Otakudom/ContReal/contReal.htm
- nhgiang 4mo ago
  That’s rad
- claw-el 4mo ago
  >”Oh, what's the unit? Do I care? I'm no fscking physics major!" lol
  - ontouchstart 4mo ago
    42! https://live.lean-lang.org/#codez=CYUwZgBAhgdgzgdxAJwgLgLwQCwCYBQAxAMYAWIxA1tPEskQA7ICWMALjYivvkA https://live.lean-lang.org/#codez=CYUwZgBAhgdgzgdxAJwgLgLwQC... (I am fscking physics major! ;-)
dilawar 4mo ago
When I was in college, I posted a question on math.se about possibility of universal gates like NOR and NAND in multi-level logic. Someone found it interesting and posted it on the mathoverflow in more mathy language . To my surprise, Terry wrote an answer to that question. I still don't get it but I was flexing the whole month. Terry also took time to respond to comments I posted on his blog and on his google wave posts (I am old). Most of them were incredibly stupid but he took time to respond. Imagine a field medalist responding to a wannabe kid living somewhere in India. Some of his real analysis notes were published in India that were cheaply available. I learnt about open/close set and convergence/cauchy series from it. I never thought I'd enjoy reading pure mathematics. Another mathematician I found very readable Daniel Spielman (I think it was his notes on smooth analysis). I once picked a book by William Tutte from the library! Never seen a book that was harder to read. I don't know what the point of my post is.
- andyferris 4mo ago
  The brilliance of a mathematician like Terry is the the clarity they can bring. That’s my interpretation of your comment, anyway.
- brookst 4mo ago
  Your point is contextualixing the humans involved, and it is a good and righteous post.
- thmorriss 4mo ago
  google wave!!! so good
  - energy123 4mo ago
    Developed by Terry's older brother at Google
sylware 4mo ago
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.

192 points by Tomte 4mo ago

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.

nylonstrung 4mo ago

More accurate title would be "Terry Tao Became an Evangelist for Lean"

vitriol83 4mo ago

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.

ruilov 4mo ago

the smartest people see AI as an incredible tool that enhances their productivity.

big-chungus4 4mo ago
Just like me! I like AI because of how smart I am.
- bigfishrunning 4mo ago
  I'm suddenly missing the slashdot mod system. +5 funny.
llamacld 4mo ago
[dead]
Jtarii 4mo ago
There is more to life than productivity.
- fasterik 4mo ago
  Productivity is relative to whatever we value. That could be building things, making art, making scientific discoveries, or delivering food to people in poverty. Maybe you value non-tangible, non-durable things like experiences. That's great, but it would be weird to tell someone who's devoted their life to X "there's more to life than X." (Replace X with any of the fields mentioned above.)
  - brookst 4mo ago
    And experiences absolutely benefit from productivity improvements. AI has helped me plan better trips, find places and activities I had no idea about, better prepare for weather in remote destinations. It’s said that “productivity” is mistakenly connoted as scoped to work.
  - Jtarii 4mo ago

klmarks 4mo ago

Quantamagazine is essentially Renaissance Fund, which is heavily invested in AI. This is a clever piece reminding people of Tao's pre-AI Lean efforts. Now, however, Tao and especially Gowers are receiving AI money and have AI positions so they are far from unbiased. Or maybe they have caught Feynman's "computer disease"? Either way, this is a hype piece.

TimorousBestie 4mo ago
Tao doesn’t seem to have been all that corrupted by the AI money. He’s signatory to the Leiden Declaration after all.
- bmitc 4mo ago
  Doesn't that require you to just click a few buttons? It's not like it's a binding pledge.
YeGoblynQueenne 4mo ago
Ahem. Define "Pre-AI". Automated theorem proving has been an AI task right from the very beginning with Simon and Newell's Logic Theorist, presented at the Dartmouth workshop in 1956. Logic Theorist soon proved 38 of the first 52 theorems in chapter 2 of the Principia Mathematica. The proof of theorem 2.85 was actually more elegant than the proof produced laboriously by hand by Russell and Whitehead (2026-03-20: What is called here Theorem 2.85 is, in fact, numbered as 2.53 in the page 107 of the 1963 Cambridge University Press edition (https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_Mathematica_vol1.pdf https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_M...) and which appears, under the same 2.53 number, on page 112 of the 1910 CUP Edition, according to the digitalization on wikibooks (https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Principia_Mathematica/Part_1/Section_A#Discussion_2 https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Pri...)). Simon was able to show the new proof to Russell himself who "responded with delight".[17] They attempted to publish the new proof in The Journal of Symbolic Logic, but it was rejected on the grounds that a new proof of an elementary mathematical theorem was not notable, apparently overlooking the fact that one of the authors was a computer program.[18][17] https://en.wikipedia.org/wiki/Logic_Theorist#History https://en.wikipedia.org/wiki/Logic_Theorist#History Maybe some people only understand "AI" to mean "LLMs" but, particularly in maths, LLMs ain't going nowhere without a symbolic solver (or a human mathematician) verifying their output.

cryo32 4mo ago

And I thought it was cocaine.

YeGoblynQueenne 4mo ago

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. _____________________ [1] https://youtu.be/cdflu9ZXZGE?si=f1xi65r7kZM8s1JI https://youtu.be/cdflu9ZXZGE?si=f1xi65r7kZM8s1JI

pfortuny 4mo ago
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.
- fn-mote 4mo ago
  I won’t downvote this thread but … the first paragraph of the article explains how Tao won some $3m award. Unless the going rate for AI-shilling is much higher than I can believe, the amount of money just is not going to be enough to get a world-class figure to suddenly sell out. If you saw him selling his morals regularly in the past, ok I’ll listen to the evidence. But suddenly now? After so long writing (essentially for free) and building community? Doesn’t make sense.
  - fragmede 4mo ago
    A $100,000 investment into Anthropic or OpenAI a few years ago would be worth a couple hundred million today, so $3m is ~nothing in that scheme of things.
  - nilkn 4mo ago
    I don't think Terence Tao sold out. However, just looking at it from OpenAI's perspective, this kind of advertising is almost certainly worth at least one order of magnitude more than $3M to the company.
    - Quarrel 4mo ago

brcmthrowaway 4mo ago

It seems Cameron Zwarich has also joined OpenAI Is there a Lean/OpenAI connection?

saagarjha 4mo ago
Where did you see that?

gosub100 4mo ago

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.

317070 4mo ago
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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- gosub100 4mo ago
  Thank you for this.

pvillano 4mo ago

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.

jplusequalt 4mo ago
>A programmer It won't be a programmer doing this work, because they will have gone the way of the dodo. It'll be workers specific to a certain domain (e.g. engineer, architect, accountant) doing this on top of their usual work. The software industry will collapse.
- CuriouslyC 4mo ago
  The architect/accountant won't be doing it either, they'll just be a liability lightning rod for people who are closer to devs than architects doing the actual day to day work. Sort of like a doctor will "manage" a team of nurse practitioners.
  - whattheheckheck 4mo ago
    Except medicine is 1000x older than software engineering as a field
xpct 4mo ago
I'm sure a system that could do this is economically optimal. Why are you looking forward to this, though?
- AndrewKemendo 4mo ago
  Not the OP but for me it’s: more optimized than any human could ever hope to write, along with a lean proof of its correctness.
4mo ago

dvt 4mo ago

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.

jplusequalt 4mo ago
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.
- dvt 4mo ago
  > pushed for by the same fucking people who caused our societies smartphone addiction Not sure where you live, but I would guess the West (where we have the luxury to be worried about "smartphone addiction"). I assure you that the net positive of smartphones, especially cheap Androids, have had a significantly more positive effect on society than negative, particularly in the developing world.
  - jplusequalt 4mo ago
    >But I assure you that the net positive of smartphones, especially cheap Androids, have had a significantly more positive effect on society than negative, particularly in the developing world. My point is that the tool which was meant to augment one particular aspect of life, has metastasized into being a cancer on many other aspects of our lives, and that has downstream consequences on society as a whole. Keeping this in mind, being a bullish on AI seems foolish. edit: Perhaps a better thesis for my reservations with rapid technological progress: smart phones were supposed to help us adjust to society, but society instead adjusted to them. AI is positioned to do the same, and we need to ask ourselves what those changes could look like, and if they're for the better, or for the worse. >where we have the luxury to be worried about "smartphone addiction" I reject this, and any similar framing that amounts to "because there are other, greater problems at play, worrying about this relatively lesser problem is worthless." A problem that impacts people is a problem that deserves attention, especially if an absolute terms the number of people impacted are in the tens/hundreds of millions.

arjie 4mo ago

Woah, guys, the article is actually super cool. I almost didn't read the article because of the AI thing - I follow him on the microblog networks and I know he's pretty good at using LLMs and so on so that's not interesting. The unique stuff about him and gowers that it points out is there idea for massively parallelizable mathematics problem solving. It's definitely worth a read for how they got the first Polymath publication and afterwards for how they want to use LLMs et al. to do this: > He predicted that in the future, instead of working alone or in small teams of two or three, mathematicians might work on projects with hundreds of other people at a time. And when these collaborations were over, he said — in his modest, understated way — the results might be checked not by human referees but by computers. Fascinating stuff. My thought has always been that the AI will accelerate individuals and we'll get something like the economy for music or sports (the top few take almost all the revenue) but this may seem like an alternative pathway that might well develop (if only in Mathematics there) where AI systems drop the coordination cost to near zero by making checking cheap. So far, and I am not foolish enough to say forever, agents are great at operating in the space of checkables and it's hard to get uniqueness out of them (I haven't succeeded in getting a real laugh from Fable) but perhaps there's a whole class of problems that we can now solve by turning humans into the search units. I love it!

InkCanon 4mo ago
The checking has nothing to do with AI, despite the (massively funded) marketing done to make you think so. It is based on formal methods/theorem provers.
- dellamonica 4mo ago
  The point of the AI with respect to checking is to translate a natural language theorem and its proof into the formal system. Most of known math is not formalized because it is very hard to do so.
- world2vec 4mo ago
  From what I've seen on Tao's YouTube channel, he does use GitHub Copilot via VSCode to write Lean4 code.

bsoles 4mo ago

As much as I like Terrence Tao, I think he is entering the crackpot phase of his career. Much like Roger Penrose and many mathematicians and physicists before him.

rowanG077 4mo ago
Wild take, without even substantiating it with a single statement.
justanotherjoe 4mo ago
Yeah mathematicians tend to do that. Physicists not so much I think. However, none of what he says about AI is such a strong prediction, unlike the 'crackpots' that are probably on your mind.
- limflick 4mo ago
  That's what all the Physicists tell me.
- cryo32 4mo ago
  As a mathematician who was married to a physicist, I disagree :)
gameshot911 4mo ago
And maybe we should listen to him...

spondyl 4mo ago

I guess fandom is just in Terry's DNA: http://shanghikid.50megs.com/Otakudom/ContReal/contReal.htm http://shanghikid.50megs.com/Otakudom/ContReal/contReal.htm

nhgiang 4mo ago
That’s rad
claw-el 4mo ago
>”Oh, what's the unit? Do I care? I'm no fscking physics major!" lol
- ontouchstart 4mo ago
  42! https://live.lean-lang.org/#codez=CYUwZgBAhgdgzgdxAJwgLgLwQCwCYBQAxAMYAWIxA1tPEskQA7ICWMALjYivvkA https://live.lean-lang.org/#codez=CYUwZgBAhgdgzgdxAJwgLgLwQC... (I am fscking physics major! ;-)

dilawar 4mo ago

When I was in college, I posted a question on math.se about possibility of universal gates like NOR and NAND in multi-level logic. Someone found it interesting and posted it on the mathoverflow in more mathy language . To my surprise, Terry wrote an answer to that question. I still don't get it but I was flexing the whole month. Terry also took time to respond to comments I posted on his blog and on his google wave posts (I am old). Most of them were incredibly stupid but he took time to respond. Imagine a field medalist responding to a wannabe kid living somewhere in India. Some of his real analysis notes were published in India that were cheaply available. I learnt about open/close set and convergence/cauchy series from it. I never thought I'd enjoy reading pure mathematics. Another mathematician I found very readable Daniel Spielman (I think it was his notes on smooth analysis). I once picked a book by William Tutte from the library! Never seen a book that was harder to read. I don't know what the point of my post is.

andyferris 4mo ago
The brilliance of a mathematician like Terry is the the clarity they can bring. That’s my interpretation of your comment, anyway.
brookst 4mo ago
Your point is contextualixing the humans involved, and it is a good and righteous post.
thmorriss 4mo ago
google wave!!! so good
- energy123 4mo ago
  Developed by Terry's older brother at Google

sylware 4mo ago

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.