Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

“Erdos problem #728 was solved more or less autonomously by AI”

mathstodon.xyz

Post reply on HN
Print view View original

31–40 of 385 posts

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#31

Post by abdullahkhalids »

lwansbrough wrote: post #14

Can anyone with specific knowledge in a sophisticated/complex field such as physics or math tell me: do you regularly talk to AI models? Do feel like there's anything to learn? As a programmer, I can come to the AI with a problem and it can come up with a few different solutions, some I may have thought about, some not. Are you getting the same value in your work, in your field?

I work in quantum computing. There is quite a lot of material about quantum computing out there that these LLMs must have been trained on. I have tried a few different ones, but they all start spouting nonsense about anything that is not super basic.

But maybe that is just me. I have read some of Terence Tao's transcripts, and the questions he asks LLMs are higher complexity than what I ask. Yet, he often gets reasonable answers. I don't yet know how I can get these tools to do better.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#32

Post by observationist »

chmod775 wrote: post #11
malux85 wrote: post #4

Earlier quoted context omitted.

This is what has excited me for many years - the idea I call "scientific refactoring" What happens if we reason upwards but change some universal constants? What happens if we use Tao instead of Pi everywhere , these kind of fun questions would otherwise require an enormous intellectual effort whereas with the mechanisation and automation of thought, we might be able to run them and see!

I can write a sed command/program that replaces every occurence of PI with TAU/2 in LaTeX formulas and it'll take me about 30 minutes. The "intellectual effort" this requires is about 0. Maybe you meant Euler's number? Since it also relates to PI, it can be used and might actually change the framework in an "interesting way" (making it more awkward in most cases - people picked PI for a reason).

I think they mean in a more general way - thinking with tau instead of pi might shift the context in terms of another method or problem solving algorithm, or there might be obscure or complex uses of tau or pi that haven't cross-fertilized in the literature - where it might be natural to think of clever extensions or use cases in one context but not the other, and those extensions and extrapolations will be apparent to AI, within reach of a tedious and exhaustive review of existing literature.

I think what they were getting at is something like this: The application of existing ideas that simply haven't been applied in certain ways because it's too boring or obvious or abstract for humans to have bothered with, but AI can plow through a year's worth of human drudgery in a day or a month or so, and that sort of "brute force" won't require any amazing new technical capabilities from AI.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#33

Post by D-Machine »

TeMPOraL wrote: post #27
D-Machine wrote: post #17

Earlier quoted context omitted.

It could not be done without Aristotle ( https://arxiv.org/pdf/2510.01346 ), as clearly described in Tao's posts.

Aristotle is an LLM system.

"Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver"

It is far more than an LLM, and math != "language".

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#34

Post by D-Machine »

doormatt wrote: post #28
D-Machine wrote: post #16

Earlier quoted context omitted.

It could not be done without Aristotle ( https://arxiv.org/pdf/2510.01346 ), did you even read the links?

And this is Aristotle - https://aristotle.harmonic.fun/ It's an LLM.

"Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver"

It is far more than an LLM, and math != "language".

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#36

Post by svat »

For context, Terence Tao started a wiki page titled “AI contributions to Erdős problems”: https://github.com/teorth/erdosproblems/wiki/AI-contribution... (as mentioned in an earlier post https://mathstodon.xyz/@tao/115818402639190439) — even relative to when he started this page less than two weeks ago (Dec 31), the current result (for problem [728]) represents a milestone: it is the first green in Section 1 of that wiki page.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#37

Post by ComplexSystems »

observationist wrote: post #2

Reconfiguring existing proofs in ways that have been tedious or obscured from humans, or using well framed methods in novel ways, will be done at superhuman speeds, and it'll unlock all sorts of capabilities well before we have to be concerned about AGI. It's going to be awesome to see what mathematicians start to do with AI tools as the tools become capable of truly keeping up with what the mathematicians want from…

If this isn't AGI, what is? It seems unavoidable that an AI which can prove complex mathematical theorems would lead to something like AGI very quickly.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#38

Post by bgwalter »

Arainach wrote: post #35
bgwalter wrote: post #21

[flagged]

Whether powered by human or computer, it is usually easier (and requires far fewer resources) to verify a specific proof than to search for a proof to a problem.

Professors elsewhere can verify the proof, but not how it was obtained. My assumption was that the focus here is on how "AI" obtains the proof and not on whether it is correct. There is no way to reproduce this experiment in an unbiased, non-corporate, academic setting.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#40

Post by mkl »

ComplexSystems wrote: post #37
observationist wrote: post #2

Reconfiguring existing proofs in ways that have been tedious or obscured from humans, or using well framed methods in novel ways, will be done at superhuman speeds, and it'll unlock all sorts of capabilities well before we have to be concerned about AGI. It's going to be awesome to see what mathematicians start to do with AI tools as the tools become capable of truly keeping up with what the mathematicians want from…

If this isn't AGI, what is? It seems unavoidable that an AI which can prove complex mathematical theorems would lead to something like AGI very quickly.

This is very narrow AI, in a subdomain where results can be automatically verified (even within mathematics that isn't currently the case for most areas).
Post reply on HN