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.

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

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.

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

Great point, I think the argument you could make about Tao (fairly or unfairly) is he never tries to build that framework.

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.

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.

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

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.

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.

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

The vast majority of research-level pure mathematics is never going to get used in science or engineering. Obviously it is hard to predict what will be useful, but for the type of mathematics that is unlikely to be, there is a question as to why we care about it, and that almost has to come down to beauty in some sense - some mathematics gives us a new lens to look at parts of the mathematical world and others chip away at problems in more mundane ways in the hope that they inspire or contribute to new parts of mathematics that are beautiful.

Much (most?) of math consists in transmission of it (according to Thurston [1]), a 1000-page proof with no possibility of transmission is mostly useless. The proof of Fermat's last Theorem is important in itself, and adds much more than the mere result.

I am not talking about the supposed "beauty" of a proof (I do not believe in that concept, rather in "elegance", which is not the same), I am talking about the proof itself, and the insights it provides.

[1] https://www.ams.org/journals/bull/1994-30-02/S0273-0979-1994...

What is the difference between "beauty" and "elegance" of a proof?

"Beauty" is something I cannot define. "Elegance", as I use it, is the use of tools as precisely as possible. It is a technical term, whereas "beauty" I cannot define.

Of course, that is my view of it.

When writing code I also believed in the "beauty" and "elegance" because IMO it opens up all kinds of different opportunities that involve using or organically growing or improving that code. It turns out that if it doesn't solve a quantifiable problem, (mostly) nobody cares. And the pace of innovating in the field outgrows the pace (by a large) of keeping things "beautiful and elegant".

Maybe English isn't your first language, but these are basically synonyms.

Maybe English is also not your first language, because they are not synonyms

You are mixing a lot of categories here -- beauty, verbosity, utility, elegance, insights.

Why all that when you just need one thing: truth.

An inscrutable 1000-page Lean proof may have low transmissibility amongst humans, yet extremely high transmissibility amongst AI mathematicians.

Probably AI mathematics needs a specially constructed or trained translation or compression system (likely also an AI system) that helps transmit dense Lean proofs back into human-style thinking. We may even see an entire field develop around creating human-comprehensible compressions of vast formal breakthroughs in mathematics. Such an activity would almost certainly be both art and science -- there's some objectivity in that certain abstractions or definitions inherently cover more ground more efficiently, yet there's also a deep creativity and artistry in finding compressions that are adapted to the specific 3+1D spatiotemporal intuition of the human mind. Perhaps with time this will keep a lot of the originality and creativity of research mathematics alive -- maybe with that work having even more centrality than it does today.

Instead of seeing this all as a loss of beauty in mathematics, I choose to see it as the beginning of a new age, which will bring entirely new problems to solve, yet also accelerate discovery at an exponential rate.

Mathematics is a language for humans, not just for machines. We may agree to let machines "do their thing" for as long as they want but to what purpose? Just creating "results"? What is a mathematical result by itself?

Unless, of course, we are willing to give machines the responsibility of building bridges. Subject on which I do not have a clear opinion yet.

But just hard drives (or whatever) filled with bytes representing strings representing nothing any human will ever understand... I am not for it (as of now). There are much more important problems to solve.

I'm not sure why we would assume that AI-generated or AI-assisted mathematics would never amount to anything useful in the real world. I would expect the opposite: the usefulness and explanatory power of mathematics has been riding an exponential over the last several centuries.

Maybe I didn't do a good job explaining it, but the rest of my prior comment was about connecting AI-generated results back into human-style thinking. Inevitably, in the far future, it's not unreasonable to assume the world will be dominated by synthetic robots controlled by artificial intelligence, and there will indeed be a point where AI builds not just bridges but vast planetary, interplanetary, and space-based infrastructure projects beyond the ability of our current civilization. At that point, mathematics may permanently move beyond the grasp of the human species. You can't teach a dog general relativity. Surely, there are truths in mathematics (and possibly physics) you cannot teach a human. Not to digress, but for me, this kind of threshold is what a term like "superintelligence" means -- the point where an intelligence is discovering truths that cannot be taught back to humans because we're not smart enough. So far, our contact with this kind of intelligence has been limited to one-off, highly specialized cases (like chess) that have little grand implication for civilization, but that won't always be the case.

But, for today and probably at least our lifetime, to make them useful major AI advances in math will need to be "compressed" back into the specific network and "towers" of concepts and abstractions that human minds specifically can understand and intuit about. So I think both directions of formalization are equally important: translating natural language statements (theorems, lemmas, etc.) faithfully into Lean and letting a theorem prover run and decoding a dense Lean proof back into natural language (which, in some ways, is the more creative and open-ended problem -- there is no one right answer).

> a 1000-page proof with no possibility of transmission

Have you actually looked at LEAN proofs? They are typically split into small bite size definitions and proofs, making it easy to dive in where you want, and skip what you don't care about, while knowing that you can trust the conclusions.

I personally think that having hundreds of mathematicians working together as a team is a beautiful thing.

> Why does it need to be beautiful?

"Beauty", IMO, signifies the idea that you're doing `something` for its own the sake where "its own sake" approximate the idea of getting/being closer to (or in proximity of) `something`/`anything`/`someone` you find "beautiful".

> Once you proved it it's true and you can use its consequences in math, sciences and engineerings (sic).

The expression "you can use its consequences in ..." suggests that the action is a "just a means" to "something else". However, not everyone is interested in the idea of "something else"; they're interested in the idea itself (in a broad sense) as that's one of the main reason they got started/involved in the first place.

---

We all do things as "just a means" to "something else". However, there must be an "end" to this chain of "something else"; otherwise, how do you find any "meaning" (or sense of fulfillment) in this whole enterprise (or chain of "something else"s)?

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.

Most mathematicians don't take pride in their results having no applications. That's just not true. Maybe some quirky pure logicians or something. But otherwise 90%+* of mathematicians I know would be at least satisfied if not thrilled for their work to be used by others.

*Completely made up statistic.

I've had the opposite experience with all the math nerds that I know. End of the day it's all anecdotal ig https://en.wikipedia.org/wiki/A_Mathematician%27s_Apology

You put it perfectly. And all these AI math startups don't actually care about mathematics. They are just using it as a proxy for general reasoning, with the VC pitch being some kind of world domination after they crack these problems.

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?

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

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.

You want to understand why it’s true, and that often correlates with beauty.

How is this relevant here? AI helps you understand the why -- it literally discovers the proof and hands it to you with explanations. It hands you the proof that you would have otherwise not found easily.

If the proof is hundreds or thousands of lines of Lean, it’s not clear that the AI will be able to provide an insightful “why”, instead of just dozens of microsteps.

And if it can provide insightful “whys”, that still correlates with beauty then.

Given the slop-like nature of what current generative AI tends to produce, I wouldn’t however count on the latter quite yet.

I don't know how you think it only gives you Lean - it gives you everything including the explanation. You can actually ask it explanation using you know.. natural language.

> And if it can provide insightful “whys”, that still correlates with beauty then.

Yeah it can, you just have to ask it. It has a good interface for it - text! I think you misunderstand how this tech works, its not just spitting out things. It has the understanding also and you can verify it by asking!

Why prove the Pythagorean theorem rather than just prove 3^2 + 4^2 = 5^2?

For any practical application, you are only interested in finite set of concrete identities, so anything beyond that is surplus to requirements, surely?

I think you may be interested in more abstract things. In this case, let's say you're creating a program for a 3D printed thing, and you have to fit a diagonal cardboard in a rectangular box, you'd like to be sure that the Pythagorean theorem holds even in cases where you haven't tried it out.

> For any practical application, you are only interested in finite set of concrete identities

I do a lot of numerical work in settings where computational efficiency is useful.

In my work, most cases you can do numerically using integration or Monte Carlo sampling or whatever.

It’s slow. It often pays to find a closed-form solution. Even if it’s just a starting point that needs refinement.

To put in terms of the Pythagorean theorem: Proving the Pythagorean theorem gives you a relationship that’s reliable, fast to evaluate, and general. Proving individual tuples gives you none of this.

That doesn’t even touch on how theorems give us a glimpse at deeper structure and truths. Proving a bunch of right-triangle tuples will probably never lead you to the rest of the identities in trig.

The current commentators are surely missing the fact that this comment is sarcastic.

You meant this as satire, right?

The cardinality of that “finite set” could end up larger than say, the number of particles in the entire universe

> Why does it need to be beautiful?

“Beauty will save the world”

> One could argue for pure mathematics that is of no practical utility

wait what is the math with no utility

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.

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

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.

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.

I'm suddenly missing the slashdot mod system. +5 funny.

There is more to life than productivity.

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

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.

Destroying all of society in the pursuit of "productivity" would be a negative thing in my opinion.

Which is why we delegate it!

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.

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.

Do you mean RenTech? Not sure how you'd know they're heavily invested in anything given the notorious secrecy of the firm. Maybe their public funds have invested in AI, but their most recent 13F shows a 23% tech sector allocation, and their public funds are maybe only half of their total AUM.

Regardless, doubting the legitimacy of Quanta bc it's a Simons Foundation initiative is foolish.

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

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.

Automath is also an early example.

> Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness.

Tao doesn’t seem to have been all that corrupted by the AI money. He’s signatory to the Leiden Declaration after all.

Doesn't that require you to just click a few buttons? It's not like it's a binding pledge.

And I thought it was cocaine.

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

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.

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.

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.

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.

I'm a Terence Tao fan, but yes, OpenAI should at the very least just be telling him to go crazy with the latest models on our dime.

No, I am not saying he has sold out: but he has the money and the contacts to see the insider-only version.

Just that. Tell my Uni to pay me 200€/month for tokens. They are just going to laugh it out.

This is my view as well. It's not like it's weird for people to get paid for things they genuinely believe in even if they were nor paid.

Maybe he’s just friggen excited about the possibilities. I’m a developer by day, and even with the pending doom of our whole craft, I’M EXCITED about what AI not only has already done for me but what I’m going to be able to do with it in the future.

Here’s one of the smarted guys who’s walked the earth, and out of his historical peers, he’ll be part of the first generation with big brains AND to have tools to give literal superhuman abilities.

Come on… TT doesn’t care about a little money for a biased plug. He could literally knock on the doors of Renascence Trading and walk in with a straight face say “give me 1% of the Medallion Fund, I start today, an office with a nice window if possible”. And it would still come off charming like he always is.

Thanks for not downvoting the thread I guess, but I don't think that's how it works. If you take someone's money to say their product is great, even if you genuinely believe it, you shouldn't be trusted. There is such a thing as conflicts of interest after all and it is not measured by the amount of interest; not least because it's hard to know what that means. It suffices that there is interest.

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

We don’t even need to know addition to understand quid pro quo. (edit Okay we may have to understand both plus and minus here. But that’s it.)

Terry has always been curious & temperedly bullish on LLMs long before OpenAI gave him any money.

Quid pro quo or not, he got paid to say what he's already been saying for the last few years.

This could be true but, no matter what, a streetwise person would never trust him after he has taken the money. If he wanted his opinion on AI to be trusted then he should have made his money some other way.

Character assassination is not a replacement for a good argument. But hey, I'm sure you get a rush from that sense of righteousness.

The "good" argument is that people trust other people's opinion more who have not been paid to advertise. I trust the doctor who personally recommends a drug more than the doctor who was paid to recommend the drug - even if they recommended the drug before they were paid. That's a fact of life, it's not "character assassination". Tao didn't do anything wrong by making an ad but he can't expect people to take his opinion seriously after someone gave him a lot of money to state an opinion that favors them.

It's proper to suspect arguments that are motivated by self-interest. The stronger that self-interest, the more one should suspect the argument. This is what you're saying?

In that case, the anti-AI Luddite arguments are maximally impeached, since they are motivated by fear of personal disaster. Tao doesn't need AI to succeed; the Luddites desperately need it to fail. So they are willing to say anything, jumping right to ad hominem arguments when they lack any real substantive rebuttal.

The billionaires shall inherit the Earth, for they are minimally of want and need, only merely aspiring for more accumulation of wealth as a sport.

Or, we can judge what they say by the merits rather than hypocritically applying ad hominem arguments to them and not to others.

It’s not an ad hominem.

I don’t know that Terry much cares about the opinions of people who judge claims based on innuendo and cynicism rather than the actual merits of the claim.

They stated a completely general principle of trust, not tied to any person or character trait. That’s not character assassination.

>> "Tao has sold out to the AI grifters to prop up the AI hype bubble" is not a take I expected to see.

To clarify there was nothing like that in my comment above.

Historically it's a little irregular for someone like that to get involved commercially at this level, but the unfortunate reality is that academic research at all levels is facing a drastic loss of funding and political support right now. They are going to have to do some things that they haven't had to do before, just to survive.

If that means that researchers like Tao have to work as consultants or adjuncts to OpenAI or other model developers, well... that's what the American people voted for when they elected Trump.

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.

Do you have any evidence that he took their money?

It seems Cameron Zwarich has also joined OpenAI

Is there a Lean/OpenAI connection?

Where did you see that?

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

Thank you for this.

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.

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.

Except medicine is 1000x older than software engineering as a field

I'm sure a system that could do this is economically optimal.

Why are you looking forward to this, though?

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.

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.

Fully automated testing + revision loops are super cool and def something I want to play with

And PBT is so close to language level invariants/preconditions/post-conditions that I dream of

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

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

Have you actually written proofs in Lean with your professional reputation on the line?

> A programmer translates a natural-language spec into a machine-readable spec

Why do we need a human for this?

Liability, and it's the hardest part.

...and no human will be able to understand the algorithm either.

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.

So maybe we will understand the algorithms

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.

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.

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

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

Social constructivism is tougher and tougher than “just tools.” Could the so-called “addictiveness” consist partly of the many other devices smartphones replaced? Sure, some attention economy but also just turn off the data?

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

This is true of all important tools in history. From computers, to electricity, cars, steam, even agriculture. They reshape society and its practices. This has been documented multiple times. One I can remember on top of my head, but is not limited to, is historical materialism.

From an misesian perspective, this seems fairly obvious:

1. smartphones are extremely useful (being miniature computers and all);

2. people tend to optimize their actions with the best tools available (i.e. smartphones in this case);

3. people will see others using smartphone increasing and will try to leverage that for their own goals, thus further adopting smartphones (even if indirectly);

4. the economy is the sum of human action, so this progressive adoption changes the economy and the culture.

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

The real issue with your post is that you seem to be trying to fix smartphones addiction by getting rid of phones, ignoring the benefits they brought and the previous problems they fixed.

Also, every problem impacts people.

>The real issue with your post is that you seem to be trying to fix smartphones addiction by getting rid of phones, ignoring the benefits they brought and the previous problems they fixed.

No, my post is decidedly not that. I'm saying maybe we should stop and think about the consequences and plan accordingly.

My bad, then. If I may suggest something, give a small acknowledgement and avoid words such as "cancer", which is pretty loaded.

Still, people (as in most individuals in the economy) can't simply be stopped, even less so to plan, specially in a free system such as enjoyed by most of the west. That requires a high degree of coordination and coersion that I think only Cuba and NK are currently capable of, slightly. Otherwise, people will just do their own thing, leading to a technological revolution again, given the material means.

A more practical approach is to continuously nudge the direction of change towards a better direction, constantly reevaluating approach, but avoiding having to stop everyone else.

> 1. smartphones are extremely useful (being miniature computers and all);

Whether they are extremely useful or just some tool that has its uses depends a lot on your lifestyle.

> 2. people tend to optimize their actions with the best tools available (i.e. smartphones in this case);

What "best (tools)" means for you, depends a lot on your values. For example, if you value privacy, mobile phones and in particular smartphones are incredibly bad tool choices.

> Whether they are extremely useful or just some tool that has its uses depends a lot on your lifestyle.

The "useful" then didn't refer to the individual value judgments of all individuals, but the presence of material affordances that a sufficiently big mass of people would find useful. I admit this was not the best wording, but I forgot (and can't find it right now) the formal term that encapsulates the material qualities that others may see usefulness.

> What "best (tools)" means for you, depends a lot on your values. For example, if you value privacy, mobile phones and in particular smartphones are incredibly bad tool choices.

Agreed, but this misses the point. I didn't mean to imply that the value of things are objective (this is a misesian perspective, SToV is implied), but that some people would find smartphones useful, adopting themselves, and that would further expand the opportunities smartphones are useful to others, creating a positive feedback loop.

I come from a developping country, and this whole schtick about "being concerned by tech addiction is a western luxury" is tiring.

As a person from the developing world I feel obligated to say that I find your assurance quite unconvincing: the negative effects of smartphone at this point in time is invariant globally, and whether they are a net positive or negative is at least debatable.

And in relation to your first comment, most sane people would agree that "tools" don't exist in isolation - neither come into existence out of nowhere.

This reductionist position of treating extremely complex machines with deep social interactions as a tool like any other is objectively wrong, and I believe the reasons are highly obvious but I can expand on this if you disagree.

I'm not the person you were responding to, but I could've written the same as they did, so here's my reply:

I don't dispute that in aggregate the effect was positive. But I spend more time thinking about things which impact me directly, and I assure you that in my personal life it used to be a problem, and fixing it was an improvement.

That's an extremely broad statement to make "assuredly". I'd wager you haven't figured environmental consequences into your calculation. All the toxic waste from production is being routed to the developing world.

These fking website sure loves to pull statistics out of the rear end

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

We've been flooded with "AGI is 6 months away!" for a few years now, mostly by Anthropic/OAI/XAI, which is clearly nonsensical hype. Also, almost everyone has been walking back their previous claims that "AI will replace ~80% of white-collar jobs."

In the last decade or so I have never seen so much layoffs across the industry. This may be suggesting that evidence supporting the latter hypothesis is not maybe too far fetched.

Do we have to rehash CEO statements about causality versus objective reality yet again?

Objective reality is that many people have lost and are still loosing their jobs. If you don't have anything useful to add to your response please refrain from polluting the discussion.

Likewise with your "may be suggesting" unfounded correlation speculation.

No, it is not the same at all. I intentionally frame my words by saying that after all there may be an indication that such an event or correlation exists but I am explicitly not stating anything, therefore it is rather an invitation for discussion and not one-sided talk.

In the last decade, the software engineering industry has turned into a grift that has pushed out hundreds of thousand of low-quality "engineers" through coding bootcamps or online courses. Many of these people have no passion for the craft or interest in building products.

Then, when money was cheap during COVID, companies over-hired unscrupulously. Now, given that markets are cooling off and there's some political, geopolitical, and economic uncertainty, companies are hedging their bets, and laying off is usually the right move, especially as interest rates are going back up.

There are perfectly viable explanations for the situation the industry finds itself in without invoking the AI boogeyman, especially considering that just about every study out there shows that AI use correlates with a fairly modest increase in productivity, and that it won't turn anyone into a "10x engineer" overnight.

Over-hiring could be one way of explaining the effect we are seeing, however, where are those "coding bootcamp" or "online courses" engineers? I honestly ask because I have never worked with one in almost 2 decades of being in the industry, and I worked across many different domains. What I see is on the contrary - the people who are getting laid off are people with legit engineering degrees from legit engineering Universities.

Also, over-hiring by the very definition implies a sudden surplus of engineers on the market. I can't quite understand where did these engineers all of the sudden come from? The number of engineers outputted by the Universities YoY is pretty much close to O(1) so I am not convinced to this theory at all and I see it only as a good excuse that companies are making in order to make them look better.

I spoke with my friends few days ago, and one of them runs the company so he asked me on the opinion of the AI frenzy. I gave him my view and by the end of it he told me that he feels uneasy but that he has to let go part of his employees because he simply does not need them anymore - they are literally replaced by the AI model and one or two or N-M engineers operating the model. Yesterday he needed 10 people for the job, today it is 2 or 3 people.

So, I think that the AI has already changed the landscape dramatically, and what we are seeing are not the post-COVID effects.

Where I'm from and peripheral countries, the industry is riddled with bootcampers and button pushers. My company even has a big bootcamp for reconversions

What are you trying to suggest? That people without the University degree who have been trained for monkey coding do exist? Sure but that's not what I was saying nor does it skew the picture in any significant way.

What I'm trying to convey and you fail to understand is the picture you have in your mind is very much affected by your reality. The fact that you don't see these bootcampers doesn't mean they don't exist.

Not only you don't have a depth of thinking critically, and understanding my point, but you're also unbelievably arrogant.

The only thing I did was to point out that anedoctal data doesnt give you the full picture. Why the insults though?

As I said, your communication style is coming across as arrogant and disrespectful. Instead of asking for more clarification and giving a benefit of a doubt you chose to counterpoint with a trivial example, in which tbh I am hesitant to believe. I say this as someone who has worked across continents and across many different domains. None of the layoffs taking place do not involve laying off "bootcamp" people.

> Instead of asking for more clarification and giving a benefit of a doubt you chose to counterpoint with a trivial example

I didn't counterpoint with a trivial example I just pointed out that where I'm from there are some bootcamp people being layed off. If you don't like someone counter pointing you, sorry that's your problem not mine. I was neither disrespectful or arrogant.

> None of the layoffs taking place do not involve laying off "bootcamp" people.

And how am I the arrogant one here? You're full of absolutes and certainties and get pisssy when someone argues against your point.

Arrogant? I believe what I am saying is factual and pretty easy to check, if not already widely known if you read at least a tiny bit of tech news - so how about layoffs in Oracle, Intel, Meta, Microsoft, Amazon, PayPal, Cisco, Dell, Atlassian, Epic Games, ASML, Verizon, ..., and this is all without mentioning startups because there's just too many of them and not many people know a lot about them etc. Which of these layoffs are the bootcamp people?

The problem I have with your "argument" is that it is unsubstantiated. And I already answered you earlier - it does not matter if such people exist because such people are not majority, unless you would like to support that hypothesis with some fact?

I know this might be shocking but... You know there are other contries besides USA? There are layoffs in other countries as well? What? Yes I know wow such a suprise. Go look at a map once in a while. Now you can call me arrogant

I'm not doxxing myself by sending you news from my country.

> if such people exist because such people are not majority

Which is different from your absolute "there are none" argument.

I live in Europe btw, and I am surrounded by people being layed off and none of them are the "bootcamp" developers. So, in order to support your view you'd really have to be more concrete, otherwise your response reads as short-viewed or even manipulative.

https://www.normaltech.ai/i/201537309/the-stories-of-ai-driv... suggests AI is used as an excuse rather than being a real reason.

Ok what's the practical difference? The layoffs are still happening.

If "the latter hypothesis" of parent commenter was that "AI will replace ~80% of white-collar jobs", then that hypothesis clearly not supported by the current layoffs. AI isn't replacing workers, AI just happens to be an easy excuse for it. Could as well have been "COVID" or "tariffs" or "the economy" or "the end of Zero interest-rate policy"

Why not? I have literally got several first hand examples where people are fired because of how good the AI models became. Why do you find that questionable?

Intriguing. You should notify Narayanan and Kapoor so they can update their post with your counter-example :)

I don't even know who those guys are. I am simply sharing my experience.

> Also, almost everyone has been walking back their previous claims that "AI will replace ~80% of white-collar jobs."

They started walking those claims back right around the time someone tried to set Sam Altman's house on fire.

Not making those claims anymore doesn't necessarily mean they don't still believe those claims, it is very possible they just realized saying the quiet part out loud was a bad look for them even if it was/is what they believed to be true.

Cool. That’s a new FUD line.

Well, there is the third type of person who plays the stoic and calls all others irrational or emotional.

There are links posted here with Tao doing OpenAI ads, that is hardly "twisting themselves into knots".

But the deflection of the day is that "AI is just a tool".

It's not deflection to take a reasoned stoic sense.

That's just nonsense being pushed by social media to convince you to be upset (or ecstatic) about something.

Calling my position stoic is kind of goofy imo (and fwiw, I personally find AI to be a pretty useful tool), but I'm not going to reply to some drive-by account literally made just to troll me.

>in the new era of "proof abundance", it is increasingly important that we also debate the "soft" aspects of our field, such as our goals and values.

Trying to upgrade the trolling to rational discourse, TT recently opined

https://mathstodon.xyz/@tao/116681024360293007

Both the Leiden Declaration[1] as well as Commelin et al.'s announcement (Shaping the Future of Mathematics in the Age of AI)[2] are completely common-sense pieces, neither overstating the power of AI nor understating the capability of these tools to be misused (most acutely when it comes to attribution).

I do think that ethically, OpenAI and Anthropic, by training their models on the entire corpus of human knowledge, have certainly broken some rules, but these rules were already broken decades ago by Google—unless we really want to start splitting hairs about if indexing + processing is different than training, which is imo a distinction without a difference—, so it's hard to see who to exactly blame. In any case, that cat is out of the bag. (And for the record, I'm technically a stakeholder: I'm part of like two class actions because of a few books I wrote.) But that's neither here nor there.

[1] https://leidendeclaration.ai/#declaration

[2] https://arxiv.org/pdf/2603.24914

I see Ochigame in both and they do talk about supply chain security..

Which Tao is more equivocal about as 2 issues higher on his mind are

1. Funding, short and long term (so he is evangelising "at the bequest of" SAIR)

2. Indigestion from generative abundance (this has always been an issue but now even researchers with permanent positions are affected, over and aside of administrative responsibilities )

here he tries to redirect attention from the "harder" problem of attribution to the "softer" problem of digestion

https://mathstodon.xyz/@tao/116590271196962848

With a side effect of asking the tool-builders to reconsider what is "value"

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!

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.

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.

From what I've seen on Tao's YouTube channel, he does use GitHub Copilot via VSCode to write Lean4 code.

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.

Wild take, without even substantiating it with a single statement.

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.

As a mathematician who was married to a physicist, I disagree :)

That's what all the Physicists tell me.

And maybe we should listen to him...

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

That’s rad

>”Oh, what's the unit? Do I care? I'm no fscking physics major!"

lol

42!

https://live.lean-lang.org/#codez=CYUwZgBAhgdgzgdxAJwgLgLwQC...

(I am fscking physics major! ;-)

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

Developed by Terry's older brother at Google

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.