The Mathocalypse (scottaaronson.blog)

It also aligns with the fear that these proofs present a risk to the ecosystem by out-competing attempts at more human-readable proofs. Perhaps though we end up with more math influencers who edit and annotate these proofs to bring them back to us.

Serious question:

Why would anyone believe this (also) is not simply example N+1 of this is the worst it will ever be, as opposed to recognizing this as what will almost certainly prove to be an awkward moment, soon to be replaced by another order of magnitude of cleaner, clearer, more intelligible, etc.?

Ximm's Law: every critique of AI assumes to some degree that contemporary implementations will not, or cannot, be improved upon.

Math proofs need to produce the correct output correctly, which is not quite the same thing.

This looks like an AI IPO PR powerplay, because at this point the proofs haven't been checked and it may not be possible for a human to check them - because proofs should be clear, not horribly written and noisy.

The noise is suspicious because it's the difference between brute forcing and cognition. A human proof won't just be logically correct, it will be cognitively distilled and coherent. It may still take years to understand it, but the logical flow will be straightforward, not obfuscated.

You want the path through the maze to be as short as possible and the map to be as clear as possible.

This sounds like the opposite. There may be a genuine path through the maze, but if it's too convoluted and takes too long it will be impossible to confirm.

I think the next step is to demand that proofs either be human-scale or they prove that a human-scale proof is impossible and the machine proof is as good as it gets.

I suspect that's possible without tripping over the halting problem. (But I can't prove it.)

Isn't that just the default experience with AI these days? In small enough scale, AI models can express their ideas clearly. But the larger and more complex the ideas are, the less suitable the outputs are for human consumption. I guess AI models think too different from humans, and nobody has trained them to communicate complex ideas in the way human experts in that particular topic expect.

This proof dump reminds me of the glut of low-quality drive-by PRs overwhelming open-source repos.

I see many parallels to genAI-assisted code development. Not surprising I think.

why not get Astra to make it make sense?

> Basically the paper is so horribly written that it’s impossible to read it without AI help

This basically describes every single PR at work for the past year. Diffs of 10k+ paragraphs of comments saying nothing. Just rubber stamp and move on, nothing else you can do.

i added "use current trendy lingo" and the results were a bit less mechanical sounding. one of them included "cooked", another had "negative aura".

i used the free google ai: (deleted the examples... but they were vaguely close to what i hear my grandkids say.)

edit: neat, insta-flagged despite hundreds of non-ai comments that have never been flagged. i would have thought that hn would use some heuristics in their ai detection but i suppose not.

Ted Chiang is incredible, my favorite writer.

I also recommend "Exhalation", though that has nothing to do with AI.

Also his "Division by Zero":

https://web.archive.org/web/20111121100139/http://www.fantas...

https://en.wikipedia.org/wiki/Division_by_Zero_(short_story)

Yes! I missed the disclosure that each of these was roughly a three hour run of a single model, not an agentic swarm until reading Aaronsons post. Wow wow wow.

Im curious as to why you think that "model capabilities" and "swarms of agents" are in any way different concepts?

thats like saying it only took me 5 seconds to score a half-court shot (ignore the several hours of missed shots before)

No, haven’t you heard? Since the AI bubble began we’ve collectively decided that outcomes are all that matter. /s

But up until now, the mathematics community has valued the "prove" part much more highly than the "deliver an insight" part. Mostly because with a little work they went hand in hand.

And going from zero proofs to one proof (even a sloppy one) is a big deal regardless of whether it was written by AI or a human.

Something that often comes out is "it is about the journey, not the destination".

Many math problems are practically useless if you only care about the answer, the millennium prize about the Navier-Stokes equation is such a problem. The solution makes no physical sense, real life fluids don't follow the Navier-Stokes equations in such extreme conditions. But in the process of finding the solution, we may get insight into what will end up being really useful. The big mess that OpenAI produced is the solution no one really cared about, but it didn't deliver much of what people actually wanted.

One reason it is sometimes seen negatively despite being at least something is that it broke the incentive. Without the million dollar prize and with only the privilege of being second, people are much less likely to go for the insightful solution.

You are wrong if you consider academic incentives, funding, human nature(reproduction/survival) and capitalism.

It would be fantastic if university and science was like "here is 100M$, play around and develop some 'understanding'". However the reality is that human societies are hierarchical and currently capitalistic which implies value creation and status building.

1) the funding bodies/agencies need proof of value that you're using the resources meaningfully to be able to assign resources

2) Humans are status seeking, power seeking, resource seeking and sexual reproduction seeking. If you hold a lot of power and make decisions, you have more of all of the above.

>And I don't think that paper addresses it, but if the LLM can find a bug in Lean and exploit it to prove something, there's a good chance it will find it and not report it.

Why would it know it found a bug?

There's an entire paper claiming that many of these AI-generated Lean proofs are formulated incorrectly / mistranslated: https://arxiv.org/abs/2610.08144

It's a mixed bag I think.

For example, the statement of e.g. Fermat's last theorem in Lean should be understandable to anyone who played The Natural Number Game [0] and knows a bit of mathematics and programming. For the proof, you trust the compiler.

The statement of other theorems can be much more delicate, and the Lean formalization may require an extensive introductory section which will need to be carefully checked.

Then there are the cases where no Lean formalization is currently available, and all we have right now is an often impenetrable pdf in the OpenAI repo. I would not at all be surprised if some of those contained logical gaps.

Time will surely tell, but there are certainly doubts and lots people are very busy checking these results.

[0] https://adam.math.hhu.de/#/g/leanprover-community/nng4

> Couldn’t the Lean code just be formulated incorrectly?

I believe so, even with all the usual safeguards properly in place: https://news.ycombinator.com/item?id=49672339

> is everyone just assuming that it just be true because the Lean code checks out?

Kinda? It's only been 24 hours since they dumped 722 manuscripts on the world, most of which are apparently basically unreadable, and only some of which come with a Lean proof, which in itself is not a joy to read afaik.

I studied physics, and most of my classmates did not end up doing anything with physics. Many are in finance or insurance or programming positions. In general, studying anything challenging (from theatre to theoretical computer science) gives some specific skills and some general abilities that etsure it isn't a complete waste even if you end up doing something different.

(That said, this is not fun, and I sympathise! I'm still a student and would like to avoid finance if at all possible. Just suggesting not to drop everything if you feel like you're learning in the process.)

(I'm now personally in the position of having to choose a PhD project, and this rapid change is interacting with making long-term plans really badly. Guidance welcome!)

I think this depends a lot on what you plan to do after your PhD. Moving to industry you will likely not use the direct work of your PhD, and instead you will rely on your broad knowledge, intuition, rigor, ability to learn hard things, and extend that to bring new research developments into practice, all of which are largely unrelated to AI scooping math proofs of prize problems.

The issue is ownership, we have no means of distributing the knowledge from the AI or rewarding those who could help.

We are quickly moving to a world where all symbolic and numeric reasoning for economic purposes is performed by AI.

Hilbert's program was ultimately about humans studying the nature of mathematics. People had different opinions about whether the idea even made sense and what would be a desirable outcome.

Gödel's incompleteness also constrains human and AI mathematicians. Both just strive to prove whatever can be proven in the system they are working in.

Yes, their parents are going around saying oof, the kids definitely didn’t get it from Roblox, or YouTube, or their peers.

I'll just leave this here https://owl.purdue.edu/owl/general_writing/academic_writing/...

really? you think they don't have friends/bros/tv/etc to imitate?

Also a ton of comments in this thread: breathless frothing hype declaring mathematics is over and assuming these proofs are exactly what they claim they are at face value, giving the company with a vested interest in everyone unquestioningly believing this is all real every conceivable benefit of the doubt

more like 3/4 of the comments but yea

Having stuff explained to you in patronizing tones? How horrible Scott!

Food and shelter /s

> what problems do these people reorient towards after this?

The same problem almost every person on earth is going to have to reorient to in the next decade, which is: how do we eat and stay housed when we have no real economic value?

Pro AI blogging sponsored by ClosedAI, XTX markets and the Simons Foundation.

To some extent this was discussed in the article, and in a way I think their goal is actually the same as it was: become the first human to understand something.

It's just that we lost one of the important ways to demonstrate understanding.

priesthood

I've asked my students whether they still want to learn maths even if there will be a machine that will answer any question instantly and they will be homeless. They said yes.

(To my credit, I have warned them since more than a year ago that we will reach this point.)

They will continue to prove theorems and make discoveries, except now they will have AI to help them so hopefully progress will be faster. At the same time, new challenges will open up, for example how do you verify what the AI is doing and how do you explain it.

Math isn't about collecting random theorems, progress in math is about gaining understanding of new systems, and the theorems are guideposts to aid in that understanding.

You can prove 1000 theorems and not really increase any understanding about a subject, but gain knowledge of 1000 random facts. For example, I can write down some complicated equation and ask you "does this have a solution in the integers"? And if you do a maze of very complex and tedious algebra to show that there is a solution, you would have proved a theorem, but you would not have done much to move math forward at all.

On the other hand, if you introduce some completely new technique, say you take my equation and turn that into an algebraic surface, and then you count some special curves that live on this surface using geometric ideas, and then you show that if the number of such curves is odd, there must be a solution in the integers, and in this specific case, it is odd, so there is a solution -- well, then you have really pushed math forward and people will celebrate your proof, even though no one really cares if the equation I wrote down has a solution in the integers.

For example, there is a long history of failed attempts to prove Fermat's last theorem driving algebra and number theory forward by introducing the concept of ideals, for example, and this concept ended up much more important than whether Fermat's theorem is true or false, which is not too much more than a piece of trivia.

Or for example, the recent proof of the Poincare conjecture relies on the machinery of the Ricci flow introduced by Richard Hamilton, who then applied it to solve a number of open problems, but Perelman was able to take it even more forward to solve Poincare. So Ricci flow was massively important machinery.

For this reason, we celebrate people like Gromov, who didn't really prove that many theorems but introduced amazing machinery -- for example, the h-principle, or Gromov Compactness -- these were ideas and math is about the ideas. The ideas are then applied, using laws of logic, to form theorems.

So mathematicians will need to mine these proofs to see if there are any new techniques - new machinery - being introduced, or if the AI just used the existing machinery more efficiently. Here too, we are just looking at AI as a form of search, which it is really good at, since there are so many thousands of papers and so many ideas, that there might be a connection between two areas that lead to a solution and the human mathematician, not knowing all known results, can't make that connection. In the future, we may wonder how anyone did math without AI, much like we would wonder how anyone can be a writer without access to a dictionary or reference work. Is the AI just searching through a catalogue of known ideas and connecting them or is the AI coming up with genuinely new stuff like Ricci flow or the h-principle?

What is interesting is seeing whether we can get AI to actually discover new machinery for us. That would be huge.

And then we need to find efficient ways to detect these ideas and describe them.

Really this is very exciting and opens up whole new workstreams for mathematicians.

If it took 3h for one of them, perhaps there was a time/compute budget cutoff along with a sorting based on some relevance.

My guess would be that these particular problems were vulnerable to an attack which built on recent advances and potentially tied in something unexpected from a distant area of mathematics. "Harder" is becoming harder to define. Harder for humans is probably not harder for LLMs.

There must be an element of luck, if they ran the remaining problems again with the same time constraints presumably a bunch would be solved

I'm a research mathematician. From what I can tell, the answer is roughly comparable to: if you posed 8,000 challenging open problems to the human math community, you might expect to see 372 of them solved within five years.

Probably some combination of: some of the 372 problems were easier than the rest; the AI got lucky on these 372; there were existing papers out there in the literature which proved especially helpful for these 372; and other similar factors.

Until this is replicated, we don’t.

It would be extremely unlikely human mathematicians able to solve these kinds of problems would accept not getting credit that would set them for life professionally.

Also lean proofs are notoriously tedious and slow to write so this level of output is very likely to be from LLMs. The number of people able to understand this level of math and prove it using Lean is a few hundred at most.

How would these ideas be available to steal?

(also answered similarly to another comment; this is a common question)

There are suddenly many new solutions to problems that have resisted sustained attacks (e.g. the Uniform Games Conjecture as detailed in TFA at some length). Where do you think they are coming from? Why is there suddenly a bunch of results to be stolen?

Have you learned something from every Fields medalist's research? If so you are a member of the extreme mathematical elite and you should probably just dig into the results yourself.

You just run it again and again and again

Often times the constant (2 in this example) is a conjectured minimum, so anything below that is a noteworthy result. Think of it as breaking through some theoretical limit.

for say FFT/integer multiplication or 3SUM, we have natural algorithms that have existed a long time with a given complexity (O(n \log n) and O(n^2), respectively). Given how long these natural algorithms have been the best algorithms we have, it is natural to conjecture they are optimal. Showing an O(n(\log n)^{.99999}) algorithm exists shows that these optimality conjectures are false.

Now, there are some critiques you can have of this. Namely, it is possible that these novel algorithms have significant trade-offs that make them almost never worthwhile in practice. "Fast" matrix multiplication algorithms are typically of this form. So perhaps this all points towards a deficiency in big O notation, which can be deceptive. But, for people who care about optimizing asymptotic complexity, it is still interesting.

Many people thought it could never be less than 2. They proved that it can. What is the true value? Nobody knows, now.

to get some intuition about why this is such a big deal, look up the history of strassen's algorithm, which solved matrix multiplication in less than O(n^3). this was a truly stunning result because it seemed intuitively obvious that the output matrix had n^2 cells each of which was calculated via an independent O(n) loop over a row/column of the input matrices, so how could you do better than n^3. but once strassen proved that you could do some clever tricks and reduce the overall time to something less than O(n^3) it started an entire cottage industry of people getting better and better algorithmic bounds. the initial breakthrough was a qualitative one, independent of how much it improved things in numerical terms.

https://hideoushumpbackfreak.com/algorithms/algorithms-stras...

Tell that to the humans working on matrix multiplication who spent years of their lives getting it from n^2.3728596 to n^2.371866, only for openai to blow it away at n^2.25

Yes it was:

https://cepr.net/publications/ai-didnt-steal-the-mathematici...

Frontier theft is just faster.