64 points smilelamp 1 hour ago 76 comments

bananaflag 1 hour ago | parent

> But even if it had solved every problem in the Langlands program, to imagine that would have “solved number theory” would be as naive as saying that the construction of the periodic table solved chemistry.

Of course if you solve any existing problem, new ones appear. That's not the point. The point is that AI will be able to advance on any problem better than any human.

ivantop 1 hour ago | parent

I don’t think we know whether or not that’s true yet. Imagine a problem which requires a paradigm shift or new novel techniques to solve. There is no proof (yet) that an AI could create one.

0c3ca83 56 minutes ago | parent

Why do you believe human brains are magic? We may need some breakthroughs, but trillions of investment tends to produce those.

And it's becoming less clear over time that a breakthrough will be needed.

ForHackernews 52 minutes ago | parent

Why do you believe that LLMs are good at the same things humans are?

0c3ca83 33 minutes ago | parent

I believe that we're investing trillions into making it so.

awesome_dude 38 minutes ago | parent

It's not magical abilities - humans have proved for millenia that they can find novel solutions to problems - we have no idea how that comes to be though (which could be called magic I guess)

At issue with AI is that it's searching an existing corpus for fragments of solutions generated by humans - that's not necessarily novel, and we've not yet worked out how to make the machines actually invent.

parodysbird 23 minutes ago | parent

> Why do you believe human brains are magic?

We chose the problems to value. Literally every step of a proof is equally proved as the starting point. The choice of the starting point is what makes the problem, and it's a normative choice, which is to say it is a social choice.

portalscriptcon 34 minutes ago | parent

We have to come to terms with the reality, and we must find a way of existing with this new super tool

cammikebrown 1 hour ago | parent

ANY problem?

jnstrdm05 1 hour ago | parent

But in a human way? I don't think so. The 700+ solutions that were put out by openAI are in no way accepted as solved until humans say so. It's kind of like saying SC2 was solved when Alpha beat the best players. The professional community just went on playing much the same. Math should do the same. Just with better tools

0c3ca83 55 minutes ago | parent

Math is too boring as a spectator sport. It's funded because of its practical use.

There's going to be some hobbyists doing math in their basements, but there's unlikely to be a future for professional mathematicians.

kaffekaka 47 minutes ago | parent

Mathematics as a field will not cease to exist, and not everyone will be interested in (or qualified to) managing the fields progress and its applications.

forgotpwd16 10 minutes ago | parent

Mathematics as field won't. It is the future of mathematicians that is uncertain.

whatshisface 34 minutes ago | parent

Haha, the breaks from reality there are two, one professionals do not spend most of their time inventing proofs, and two, practical use? :-)

parodysbird 29 minutes ago | parent

> It's funded because of its practical use.

That's exactly what the Simons foundation was set up to reject, and it's one of most important funding streams for math

ion_trapper 49 minutes ago | parent

The proofs may not yet be understood, but to claim they should not yet be accepted as solved is to claim there is a bug in Lean, which is a big claim.

pitchlatte 40 minutes ago | parent

the impression i get is that people don’t per se assert that exploitable bugs exist in Lean, but that the volume of (code) proofs published represent a new magnitude of challenge to the integrity of Lean.

the obverse would be to assert that Lean (or any other theorem prover) is infallible under all circumstances, present and future - an even weightier claim in my opinion.

ericpruitt 39 minutes ago | parent

Isn't it also possible that the written proofs themselves are incorrect, say, for example, by mis-specification of constraints? Let's say I publish what I claim is a proof that 2+2=4, but in the Lean specification, I proved 1+1=2.

thevinter 14 minutes ago | parent

To be pedantic, the proofs would be correct, they would just be proving the wrong thing.

To address what you actually meant: it's possible but specifications are way easier to verify.

oulipo 8 minutes ago | parent

The main issue would rather that the formalization itself has a bug, eg. those proofs that you're trying to formalize are not "1 + 1 = 2" but theorems which take already multiple pages just to enunciate. And in these enunciations (that are made by humans) there can be errors.

In general, once the proof has been formalized, it's supposed to be the proof of the correct theorem (that's what the Lean proof-checker checks)

aktuel 28 minutes ago | parent

No. Lean being bug-free is a far bigger claim.

ion_trapper 23 minutes ago | parent

A bug which has allowed 700 proofs from diverse fields of math to appear as proven, and noone has figured it out yet?

afdbcreid 6 minutes ago | parent

A single bug can usually allow you to prove anything you want. Saying that this is how the proofs were achieved is a totally different matter though, and probably incorrect.

computerdork 15 minutes ago | parent

Hmm, am no expert at Lean, but on one hand, since it's a programming language, guessing it necessarily means like all other programming languages, it has bugs.

But on the other hand, agree with you that the chances that one its bugs causes a solved proofs to be wrong is probably very, very low. Yeah, each version of Lean obviously must be run against hundreds if not thousands tests of existing proofs to ensure it's working correctly...

... Although, one thing that is a little worrying is that some mathematicians have said the Lean code generated in these OpenAI proofs is supposedly really complex and undecipherable. It might be pushing Lean to corner cases that are not well tested.

oulipo 7 minutes ago | parent

It can possibly have bugs. That said, the "core" of Lean is a somewhat "simple" core that does simple things to check the proof, so it's quite rare to find meaningful bugs

pfdietz 13 minutes ago | parent

Plenty of these AI proofs have been accepted. On the most important result, on the Quasi-Riemann Hypothesis, there is no serious belief it's wrong. Mathematicians have already dissected and reformulated the claims.

The proof with the 11/12 constant, the simplest one, has already prompted what looks like chagrin from some. It's an unexpected combination of known results/techniques, a combination that apparently fell into a blind spot so it wasn't picked up before (even though it could have been, even 20 years ago).

I think these results are showing there was a lot of low hanging fruit that human mathematicians didn't have the breadth or mental bandwidth to find.

oulipo 9 minutes ago | parent

There's been many bugs found in Lean already, and there are probably still a few. So that's not the main issue.

stillatit 47 minutes ago | parent

I keep seeing people point to AI solved games as evidence that AI advancements are less impactful than we might think. Usually it's chess ("today there are more players than ever!"). Most of the time these are bad analogies. Games are played for entertainment, so productivity is meaningless.

I never advanced in math past high school, but my assumption would be that we as a society aren't paying mathematicians to have fun[0]. The discoveries mathematicians make must translate into real improvements in engineering and other life improving fields. So why would we pay mathematicians to work on math much the same way, if a new machine-led way makes these discoveries faster and cheaper?

[0] Being a little facetious. I know I don't know what I don't know.

jacquesm 45 minutes ago | parent

Mathematicians can have as much fun as they want while working on math problems, they have the skills and the brains, why shouldn't they enjoy their work?

With math you never know up front what 'real improvements in engineering and other life improving fields' will require some key bit of it that someone interested in pure math came up with a decade or two (or 10) before we found an application.

stillatit 20 minutes ago | parent

>Mathematicians can have as much fun as they want while working on math problems, they have the skills and the brains, why shouldn't they enjoy their work?

Obviously. In my ideal world even the janitors at the same institutions would have a blast, it's just not usually the end-goal reason humans are hired.

>With math you never know up front what 'real improvements in engineering and other life improving fields' will require some key bit of it that someone interested in pure math came up with a decade or two (or 10) before we found an application.

Right, but would it have made a difference for the application layer if that key bit of "pure math" had been discovered by a human (that had a great time) or a machine? That's my point about games being a bad analogy.

jacquesm 6 minutes ago | parent

That depends. Many of these things can only be applied safely once they're understood.

For instance, almost all of cryptography is applied math. If your opponent understands the math better than you do you might end up with your secrets compromised.

Math is about as 'pure' a science as there is, the touchstone of applicability is missing the point entirely it is first and foremost about understanding things at one of the most fundamental levels (even more fundamental than physics) that there is.

Nobody cares all that much about the discovery (except that we name things for the person that discovers it, it's sort of analogous to the discovery of a new piece of land). What they do really care about is their ability to understand the discovery and that this discovery has the proper foundations. It doesn't really matter what the answer is if you don't actually fully understand the question.

forgotpwd16 13 minutes ago | parent

Many academic disciplines bring no everyday life improvements. They exist because they provide intrinsic value and long-term foundations, hence they aren't merely entertainment. Mathematics/physics happen to be fields that span the entirety of applied/pure spectrum. Those said, your question can be generalized: Should society continue funding human intellectual activities when AI can perform them substantially better?

thrance 58 minutes ago | parent

But how do you know which problems are worth making progress on? Traditionally, you'd find those by working on solving previous problems.

whattheheckheck 18 minutes ago | parent

How do you build a society where everyone wants to live in it and has a means to?

pfdietz 10 minutes ago | parent

How do you reach the conclusion that society is something that admits rational design?

andsoitis 57 minutes ago | parent

> The point is that AI will be able to advance on any problem better than any human.

Define "better".

dooglius 54 minutes ago | parent

All but a negligible amount of novel mathematical results going forward will have had substantial LLM involvement

gavmor 38 minutes ago | parent

Define "advance"!

LLM agents are perfectly capable of "advancing" my codebase down bizarre, esoteric rabbitholes. Meanwhile, the value remains undelivered.

Many crystals, likewise, are advancing their fantastic complexities in the deep, dark recesses beneath the crust of the earth, but does it make a sound? Who gives a shit.

Many paperclips, indeed, can be churned out. Even we can be converted into paperclips, remember.

likoya 48 minutes ago | parent

Did any ai made any new interesting question or conjecture?

conartist6 43 minutes ago | parent

> The point is that AI will be able to advance on any problem better than any human.

If that was true it would of course be significant.

If you had no morals, 2 trillion dollars to spend, ability to commit intellectual property theft without consequences, and most of the smartest people in the world actively working to advance your cause... ...you really think you couldn't compete with the clankers?

joe_the_user 32 minutes ago | parent

The thing about much human progress on various problems is that human mathematicians formulate a human comprehensible machinery for the purposes of solving a given problem and then that machinery naturally suggests (to humans) further questions which then give rise to more machinery - And, in a sense, the value is ultimately the machinery, which has tended in the past to be relevant to physics, computer science, logistics, sociology and philosophy.

When AI writes proof no human can understand, it doesn't advance mathematics this way. Maybe AIs can understand their own proofs - meaning not just verify them but extract a machinery/broader-perspective (but I wouldn't count on it). But even machinery an AI isn't necessarily useful for humanity/society.

oulipo 10 minutes ago | parent

But the question is whether the AI will itself be able to decide on which problem to advance, and do it in an ethical and aligned way with humanity. And that if it does, its significance will be understood by humans.

Otherwise we're just creating a black box, easily manipulated by their owners, who would be ruling over human lives. That's not what people want

0c3ca83 59 minutes ago | parent

> But even if it had solved every problem in the Langlands program, to imagine that would have “solved number theory” would be as naive as saying that the construction of the periodic table solved chemistry.

This analogy is pants on head stupid. They're talking as though the only thing AI will ever solve is the Langlands program, not as though we have discovered a generic tool.

It's like saying "they drove the car one mile -- and every mile driven leads to more roads that we can trot along, why are you so worried about the future of horses?"

wonnage 56 minutes ago | parent

I think I’ll take the professional mathematician perception of how AI affects his field over random HN commenter saying it’s “pants on head stupid”

0c3ca83 50 minutes ago | parent

Sure, or you can think for yourself for five minutes on the implications of a general proof machine, and whether it's likely to continue producing proofs.

If you've forgotten how to think for yourself, you can also ask an LLM.

The host of the blog, Tao, was an early booster. He didn't think through the implications, and seems to have expected it to remain unable to do interesting work. Today he's on a "war footing".

I don't think mathematics are uniquely skilled at predicting the future, and the impacts of AI on their profession.

kaffekaka 40 minutes ago | parent

It is weird. From what I can tell, you and I have quite similar expectations on what AI will be able to do in the future, but for some reason you are much more dismissive of Taos opinion.

I perfectly understand his point and it is not about being selfishly frustrated by a machine being better than him. Is that really your interpretation of the discourse?

wonnage 39 minutes ago | parent

Neither are mindless AI boosters

https://fortune.com/article/ai-godfather-radiologists-obsole...

Ironic that you resort to “think for yourself” as your silly name calling go to btw

ghusto 42 minutes ago | parent

Logic is logic, you don't need a specialist's opinion on every aspect of a specialist field. I've had eye opening insights delivered to me on problems I'm working on by people who barely know how to use a computer.

wonnage 35 minutes ago | parent

You are welcome to opine on anything but there’s a reason we’re reading his blog and you’re down here in the comments

ion_trapper 25 minutes ago | parent

On the flip side, the professional mathematician has all the incentive to pearl clutch and rent seek.

sjdh76 46 minutes ago | parent

People are allowed to process their anxieties. And processing takes time. That said publicly doing it on the great modern internet attention/noise factory complicates the story.

coliveira 40 minutes ago | parent

Everyone is surprised that a person that some consider to be one of the greatest modern mathematicians can have such obtuse views of technology and its own field.

0c3ca83 32 minutes ago | parent

Note, this is a guest post.

QuesnayJr 28 minutes ago | parent

I don't think it was a particularly well-reasoned essay (I thought the classification of finite simple groups is almost evidence for the opposite of what he says), but at the same time I don't think you understood his point.

If we have a theorem proving machine, then we can use it to prove theorems. If we have a machine to solve the Langlands program in one day, then we'll think of more things to prove after that. There's a million unsolved questions in number theory unrelated to Langlands, and if we knew Langlands (and why it was true) we could make new conjectures that our theorem proving machine could solve, rather than having to speculate for 50 or 100 years like now.

The possibility he's not considering is that the machine might be better even at conjectures, and then there really is no role for humans once the machine already knows things our primitive meat brains are too small to understand. But what he's saying isn't "pants on head stupid".

qasg17 56 minutes ago | parent

Have the pro-AI people finally found a new mathematician? Otherwise it is always the same 10 people on Tao's blog citing each other.

This guest author runs a seminar to lure people into AI:

https://math.uchicago.edu/~fcale/AI.html

UltraSane 25 minutes ago | parent

Lure people? It isn't a cult.

fooker 55 minutes ago | parent

It’s amazing for me to see math research going from craft to technology.

CS had this moment decades ago, sans some theoretical parts that are joining the bandwagon now.

I did a bit of math research in grad school collaborating with my math postdoc roommate. I found the aversion to any computation making its way into the craft to be odd decades ago.

Well, now the proof’s in the AI generated pudding.

bsaul 43 minutes ago | parent

Isn't it the passage of mathematics from the age of craftsmanship to the age of industrial making ?

My recent take on AI is that people haven't adapted to the new huge potential of the tool, and don't dream big enough (yet).

It's like seeing a car engine for the first time, lamenting about the future of horses, and not realizing it'll also help us fly.

hmokiguess 29 minutes ago | parent

This is really well put, I totally agree with you.

There’s an immediate resistance towards change rather than embracing it and finding opportunities to improve and work with it.

kaffekaka 27 minutes ago | parent

Yes, this. Unless there is a true singularity where no more questions are ever asked, there will be definition be infinitely many problems to solve, and most of them we have not even glimpsed yet.

Singularity? Probably not.

Tech bro dictatorship? Unfortunately a bit more likely.

None of the above? Then we have a small shot at a great future.

Having a machine that solves hard problems must be a good thing.

disfictional 25 minutes ago | parent

Solving the hardest problems doesn't always result in the best outcomes unless the answers are shared equitably and implemented compassionately.

ethanlipson 18 minutes ago | parent

To a first approximation I agree that it’s similar to industrialization. However there’s a key factor which distinguishes this case, and which makes the analogy less than perfect: there isn’t a profit motive in mathematics, so there was no push for this development from inside the field. Instead, the industrialization was entirely exogenous, from companies which do in fact have that profit motive and view math as a means to achieve it.

There might be a “proof motive” in math which one could argue will drive the full automation of theorem proving. But we must recognize that profit is more universally valuable (i.e. it has value outside the industry in which it was created), whereas proofs are only valuable inside the math community (at least the pure math proofs the labs have been publishing thus far).

bcvvvy 10 minutes ago | parent

How you get somewhere is important and tools change how you get there.

You can drive 1000 miles and arrive at the destination on the highway quickly.

Or you can take the slow road and walk. You discover unrelated things, make new relationships, see the scenery, listen and smell what is around you and have time to contemplate things which may or not be related.

This particular tool economy robs us of all these things in the rush to the destination.

I'd sacrifice "progress" a little for some of the better bits of humanity.

kccqzy 33 minutes ago | parent

> To me, someone who chooses a worthwhile problem, obtains a proof completely using AI, understands it thoroughly, and uses it to develop interesting further questions or directions has made a substantial mathematical contribution. I would give that person substantial credit even if they supplied no new ingredient in the original proof.

Yup. This is what Terence Tao has been saying about digestion of results for several months now. Mathematics has become a field where results themselves matter less, the social aspect of attracting others to understand your results and explore new problems has become more important.

In a sense it is a little bit like software engineering, where writing code can sometimes be delegated to AI, and is arguably less important than understanding what the customer really wants from this software.

ur-whale 25 minutes ago | parent

Wake me up when AI solves Collatz.

waynecochran 24 minutes ago | parent

What is the current thought on AI creating new emergent forms of mathematics? Even the most stunning results like the proof of the quasi-RH are a clever combination of known mathematics. Humans have created (discovered?) stunning new ideas (e.g. complex numbers) that have opened wide new horizons -- do we think AI will be capable of creting / discovering novel new things like this?

stephbook 17 minutes ago | parent

Are humans going to be able to recognize the things AI discovers?

It took us a while to make the planets line up neatly in a heliocentric system. Just last month I read that a whale mother "might" grief while carrying her stillborn child.

The limiting factor is human imagination and comprehension. No offense, but see your comment.

I think AI has already invented new math, but the guys haven't looked for it because they didn't think it possible. And even under their noses, they wouldn't understand what they see.

> It's not what you look at that matters, it's what you see. —Thoreau

pfdietz 9 minutes ago | parent

> Are humans going to be able to recognize the things AI discovers?

They have been so far.

Artoooooor 23 minutes ago | parent

Just force OpenAI to un-steal the solution of Navier-Stokes problem.

Athanase000 18 minutes ago | parent

Can we stop with this ridiculous narrative? That didn't happen.

ethanlipson 8 minutes ago | parent

Why do nearly all the articles exploring the development of AI applied to math assume that capabilities won’t extend beyond theorem proving?

> other skills will matter more: choosing which terrain is worth exploring, steering fleets of airplanes, and explaining what they find to the rest of the world.

These all seem totally achievable by LLM agents, or at least, I don’t see an obvious reason why it wouldn’t be. 3blue1brown’s recent discussion on this subject was a bit better, but he spent the plurality of main body of the video assuming this scenario, devoting less time to the other possibilities. To me, it seems dangerous to build a math career on the foundation that AI won’t be able to explain math well in a few years, let alone a few months (which seems entirely plausible given the recent math progress).