“Erdos problem #728 was solved more or less autonomously by AI” • Hacker News Board

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

#141

Post by ogogmad » Sat, Jan 10, 2026, 1:24 AM UTC

malux85 wrote: post #4

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…

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'm using LLMs to rewrite every formula featuring the Gamma function to instead use the factorial. Just let "z!" mean "Gamma(z+1)", substitute everywhere, and simplify. Then have the AI rewrite any prose.

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

#142

Post by navels » Sat, Jan 10, 2026, 1:25 AM UTC

feastingonslop wrote: post #131

falcor84 wrote: post #125

Earlier quoted context omitted.

> Any talk of "AGI" is, as always, ridiculous. How did you arrive at "ridiculous"? What we're seeing here is incredible progress over what we had a year ago. Even ARC-AGI-2 is now at over 50%. Given that this sort of process is also being applied to AI development itself, it's really not clear to me that humans would be a valuable component in knowledge work for much longer.

Excellent! Humans can then spend their time on other activities, rather than get bogged down in the mundane.

Other activites such as the sublime pursuit of truth and beauty . . . aka mathematics ;-)

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

#143

Post by raincole » Sat, Jan 10, 2026, 1:31 AM UTC

XCSme wrote: post #114

TeMPOraL wrote: post #95

Earlier quoted context omitted.

> Aristotle integrates three main components (...) The second one being backed by a model. > It is far more than an LLM It's an LLM with a bunch of tools around it, and a slightly different runtime that ChatGPT. It's "only" that, but people - even here, of all places - keep underestimating just how much power there is in that. > math != "language". How so?

I kind of agree, "math" can be a "language". Same as "images" can be a language. You can use anything as tokens.

In this context, we're not even talking about "math" (as a broad, abstract concept). We're strictly talking about converting English to Lean. Both are just languages. Lean isn't just something that can be a language. It's a language.

There is no reason or framing where you can say Aristotle isn't a language model.

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

#144

Post by perching_aix » Sat, Jan 10, 2026, 1:33 AM UTC

zozbot234 wrote: post #111

bgwalter wrote: post #21

[flagged]

> ... Also, I would not put it past OpenAI to drag up a similar proof using ChatGPT, refine it and pretend that ChatGPT found it. ... That's the best part! They don't even need to, because ChatGPT will happily do its own private "literature search" and then not tell you about it - even Terence Tao has freely admitted as much in his previous comments on the topic. So we can at least afford to be a bit less curmudgeonl…

> ChatGPT will happily do its own private "literature search" and then not tell you about it

Also known as model inference. This is not something "private" or secret [*]. AI models are lossily compressed data stores and will always will be. The model doesn't report on such "searches", because they are not actual searches driven by model output, but just the regular operation of the model driven by the inference engine used.

> even Terence Tao has freely admitted as much

Bit of a (willfully?) misleading way of saying they actively looked for it on a best effort basis, isn't it?

[*] A valid point of criticism would be that the training data is kept private for the proprietary models Tao and co. using, so source finding becomes a goose chase with no definitive end to it.

An I think valid counterpoint however is that if locating such literature content is so difficult for subject matter experts, then the model being able to "do so" in itself is a demonstration of value. Even if the model is not able to venture a backreference, by virtue of that not being an actual search.

This is reflected in many other walks of life too. One of my long held ideas regarding UX for example is that features users are not able to find "do not exist".

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

#145

Post by D-Machine » Sat, Jan 10, 2026, 1:33 AM UTC

TeMPOraL wrote: post #134

D-Machine wrote: post #106

Earlier quoted context omitted.

Transformer != LLM. See my edited top-level post. Just because Aristotle uses a transformer doesn't mean it is an LLM, just as Vision Transformers and AlphaFold use transformers but are not LLMs. LLM = Large Language Model. Large refers to both the number of parameters (and in practice, depth) of the model, and also implicitly the amount of data used for training, and "language" means human (i.e. written, spoken) lan…

The paper you keep linking literally says they're using a large language model (search for that very string in it).

Sigh. If I start with a pre-trained LLM architecture, and then do extensive further training / fine-tuning with different data and loss functions and custom similarity metrics for specialized search and specialized training procedures, and use feedback from other automated systems, we are far, far more than an LLM. That's the point. Calling something like this an LLM is as deeply misleading as calling AlphaFold an LLM. These tools goes far beyond simple LLMs. The special losses and metrics are really so important here and are why these tools can be so game-changing.

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

#146

Post by zozbot234 » Sat, Jan 10, 2026, 1:37 AM UTC

Legend2440 wrote: post #138

xorcist wrote: post #51

Earlier quoted context omitted.

> Reconfiguring existing proofs in ways that have been tedious or obscured from humans, To a layman, that doesn't sound like very AI-like? Surely there must be a dozen algorithms to effectively search this space already, given that mathematics is pretty logical?

The issue with traditional logic solvers ('good old-fashioned AI') is that the search space is extremely large, or even infinite. Logic solvers are useful, but not tractable as a general way to approach mathematics.

> Logic solvers are useful, but not tractable as a general way to approach mathematics.

To be clear, there are explicitly computationally tractable fragments of existing logics, but they're more-or-less uninteresting by definition: they often look like very simple taxonomies (i.e. purely implicational) or like a variety of "modal" and/or "multi-modal" constructions over simpler logics.

Of course it would be nice to explicitly tease out and write down the "computationally tractable" general logical reasoning that some existing style of proof is implicitly relying on (AIUI this kind of inquiry would generally be comprised under "synthetic mathematics", trying to find simple treatments in axiom- and rule-of-inference style for existing complex theories) but that's also difficult.

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

#147

Post by [deleted] » Sat, Jan 10, 2026, 1:37 AM UTC

falcor84 wrote: post #125

markusde wrote: post #100

Earlier quoted context omitted.

Yes, the contributions of the people promoting the AI should be considered, as well as the people who designed the Lean libraries used in-the-loop while the AI was writing the solution. Any talk of "AGI" is, as always, ridiculous. But speaking as a specialist in theorem proving, this result is pretty impressive! It would have likely taken me a lot longer to formalize this result even if it was in my area of specialty…

> Any talk of "AGI" is, as always, ridiculous. How did you arrive at "ridiculous"? What we're seeing here is incredible progress over what we had a year ago. Even ARC-AGI-2 is now at over 50%. Given that this sort of process is also being applied to AI development itself, it's really not clear to me that humans would be a valuable component in knowledge work for much longer.

[deleted]

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

#148

Post by aidenn0 » Sat, Jan 10, 2026, 1:38 AM UTC

maxwells-daemon wrote: post #122

I work at Harmonic, the company behind Aristotle. To clear up a few misconceptions: - Aristotle uses modern AI techniques heavily, including language modeling. - Aristotle can be guided by an informal (English) proof. If the proof is correct, Aristotle has a good chance at translating it into Lean (which is a strong vote of confidence that your English proof is solid). I believe that's what happened here. - Once a pr…

How do you verify that the AI translation to Lean is a correct formalization of the problem? In other fields, generative AI is very good at making up plausible sounding lies, so I'm wondering how likely that is for this usage.

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

#149

Post by catlifeonmars » Sat, Jan 10, 2026, 1:42 AM UTC

falcor84 wrote: post #125

markusde wrote: post #100

Earlier quoted context omitted.

Yes, the contributions of the people promoting the AI should be considered, as well as the people who designed the Lean libraries used in-the-loop while the AI was writing the solution. Any talk of "AGI" is, as always, ridiculous. But speaking as a specialist in theorem proving, this result is pretty impressive! It would have likely taken me a lot longer to formalize this result even if it was in my area of specialty…

> Any talk of "AGI" is, as always, ridiculous. How did you arrive at "ridiculous"? What we're seeing here is incredible progress over what we had a year ago. Even ARC-AGI-2 is now at over 50%. Given that this sort of process is also being applied to AI development itself, it's really not clear to me that humans would be a valuable component in knowledge work for much longer.

“Much longer” is doing a lot of heavy lifting there.

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

#150

Post by amluto » Sat, Jan 10, 2026, 1:43 AM UTC

roadside_picnic wrote: post #54

sublinear wrote: post #23

Earlier quoted context omitted.

I agree only with the part about reconfiguring existing proofs. That's the value here. It is still likely very tedious to confirm what the LLMs say, but at least it's better than waiting for humans to do this half of the work. For all topics that can be expressed with language, the value of LLMs is shuffling things around to tease out a different perspective from the humans reading the output. This is the only realis…

> It is still likely very tedious to confirm what the LLMs say, A large amount of Tao's work is around using AI to assist in creating Lean proofs. I'm generally on the more skeptical side of things regarding LLMs and grand visions, but assisting in the creation of Lean proofs is a huge area of opportunity for LLMs and really could change mathematics in fundamental ways. One naive belief many people have is that proof…

If you consider the statement that perfect play by both sides in checked results in a draw to be the statement of a theorem, then the proof is 237GB compressed :) And verifying it requires quite a lot of computation.

https://www.science.org/cms/asset/7f2147df-b2f1-4748-9e98-1a...