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.
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.
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).
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.
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.
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.
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.
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.
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.
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.
You can look forward to that, but today I’m already experiencing something worse but close enough for all but the most critical code: AI-driven algorithm design + tests in your favorite property-based testing library (like OG QuickCheck in Haskell or hypothesis in Python).
Of course problems remain in both approaches: a human or AI needs to make sure the lean proof is proving the correct translation from natural language spec to a formal theorem, or the PBT is testing the right properties translated from natural language.
You don't need to check the proof. A regular proof is written to convince other mathematicians. A regular proof can skip details and contain mistakes. A formal proof cannot skip details or contain mistakes.
A lean proof is a sequence of instructions that starts with a list of facts, and combines them into new facts until a target fact is produced. Each instruction in the sequence is one of a few allowed tactics provided by lean that always produce correct facts from correct facts.
IF (1) you agree with the starting facts, (2) you are sure the target fact is what you're actually trying to prove and (3) the lean compiler says "yep, this is a valid sequence of instructions" THEN you can be sure the target fact is true.
You can be sure the final fact is true, even if you don't understand all the steps, because it's written in lean, and lean only allows steps that are free from omissions or errors
AlphaGo, through self-play, found new strategies to beat the best human players. But now that anyone can play against AlphaGo, humans are learning these strategies.
Deepmind is saying people are learning from the algorithms AlphaEvolve is generating. They say the programs tend to be short.
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.
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".
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!
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.
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.
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.
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.
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...
42 comments
[ 2.6 ms ] story [ 77.6 ms ] threadBeautiful explanations are lovely when they exist, but we shouldn't wait for them if we can also find the truth through an ugly method.
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.
wait what is the math with no utility
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.
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.
_____________________
[1] https://youtu.be/cdflu9ZXZGE?si=f1xi65r7kZM8s1JI
Is there a Lean/OpenAI connection?
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.
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...
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.
Why are you looking forward to this, though?
Of course problems remain in both approaches: a human or AI needs to make sure the lean proof is proving the correct translation from natural language spec to a formal theorem, or the PBT is testing the right properties translated from natural language.
And PBT is so close to language level invariants/preconditions/post-conditions that I dream of
A lean proof is a sequence of instructions that starts with a list of facts, and combines them into new facts until a target fact is produced. Each instruction in the sequence is one of a few allowed tactics provided by lean that always produce correct facts from correct facts.
IF (1) you agree with the starting facts, (2) you are sure the target fact is what you're actually trying to prove and (3) the lean compiler says "yep, this is a valid sequence of instructions" THEN you can be sure the target fact is true.
You can be sure the final fact is true, even if you don't understand all the steps, because it's written in lean, and lean only allows steps that are free from omissions or errors
Why do we need a human for this?
Deepmind is saying people are learning from the algorithms AlphaEvolve is generating. They say the programs tend to be short.
So maybe we will understand the algorithms
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.
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!
> 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!
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.
All that to find a path to true or false.