▲ 192 points
back
178 comments
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.
The brilliance of a mathematician like Terry is the the clarity they can bring.
That’s my interpretation of your comment, anyway.
Your point is contextualixing the humans involved, and it is a good and righteous post.
google wave!!! so good
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.
I guess fandom is just in Terry's DNA: http://shanghikid.50megs.com/Otakudom/ContReal/contReal.htm
>”Oh, what's the unit? Do I care? I'm no fscking physics major!"
lol
That’s rad
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.
>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.
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.
How would you even be able to recognize the proof is valid? Or its own proof that it understands its own proof....
This ain't the future
> A programmer translates a natural-language spec into a machine-readable spec
Why do we need a human for this?
I'm sure a system that could do this is economically optimal.
Why are you looking forward to this, though?
...and no human will be able to understand the algorithm either.
More accurate title would be "Terry Tao Became an Evangelist for Lean"
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 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.
"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.
Do you have any evidence that he took their money?
the smartest people see AI as an incredible tool that enhances their productivity.
Just like me! I like AI because of how smart I am.
You went so deep there champ
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.
There is more to life than productivity.
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.
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...
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.
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.
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".
Happy to be corrected on this!
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.
> 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?
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 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.
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 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.
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.
It seems Cameron Zwarich has also joined OpenAI
Is there a Lean/OpenAI connection?
And I thought it was cocaine.
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.