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

111–120 of 385 posts

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

#111

Post by zozbot234 »

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 curmudgeonly and cynical about that specific dynamic: we've literally seen it happen.

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

#112

Post by threethirtytwo »

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…

Math is the tip of the iceberg. If it can do proofs, it can do anything.

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

#113

Post by tachim »

dang wrote: post #75
tachim wrote: post #8

You can try out Aristotle yourself today https://aristotle.harmonic.fun/ . No more waitlist!

This deserves a HN thread in its own right! Do you want to submit it and email hn@ycombinator.com so we can put it in the SCP ( https://news.ycombinator.com/item?id=26998308 )? Edit: I just realized from https://news.ycombinator.com/item?id=46296801 that you're the CEO! - in that case maybe you, or whoever you think most appropriate from your organization, could submit it along with a text description of what it is,…

Sure! Should this be a "Show HN" or some other type of post?

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

#114

Post by XCSme »

TeMPOraL wrote: post #95
D-Machine wrote: post #33

Earlier quoted context omitted.

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

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

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

#116

Post by kortex »

MyFirstSass wrote: post #102
Davidzheng wrote: post #93

Earlier quoted context omitted.

The proof is ai generated?

Eh? The text reads: "Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver" Not saying it's not an amazing setup, i just don't understand the word "AI" being used like this when it's the setup / system that's brilliant in conjunction with absolute experts.

That's literally AI though. AI has been around formally since 1956.

https://en.wikipedia.org/wiki/Dartmouth_workshop

AI != AGI != neural networks != LLMs

But Tao did mention ChatGPT so i believe LLMs were involved at least partially.

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

#117

Post by libraryofbabel »

zozbot234 wrote: post #82
libraryofbabel wrote: post #56

2026 should be interesting. This stuff is not magic, and progress is always going to be gradual with solutions to less interesting or "easier" problems first, but I think we're going to see more milestones like this with AI able to chip away around the edges of unsolved mathematics. Of course, that will require a lot of human expertise too: even this one was only "solved more or less autonomously by AI (after some fe…

Uh, this was exactly a "remix" of similar proofs that most likely were in the training data. It's just that some people misunderestimate how compelling that "remix" ability can be, especially when paired with a direct awareness of formal logical errors in one's attempted proof and how they might be addressed in the typical case.

Then what sort of math problem would be a milestone for you where an AI was doing something novel?

Or are you just saying that solving novel problems involves remixing ideas? Well, that's true for human problem solving too.

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

#118

Post by thomasahle »

Davidzheng wrote: post #103
thomasahle wrote: post #60

It took Andrew Wiles 7 years of intense work to solve Fermat's Last Theorem. The METR institute predicts that the length of tasks AI agents can complete doubles every 7 months. We should expect it to take until 2033 before AI solves Clay Institute-level problems with 50% reliability.

If you have a sufficiently strong verifier 1/100000 reliability is already enough

Sure, but then 50% reliability just becomes a matter of whether you can make a strong enough verifier.

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

#119

Post by thomasahle »

kelseyfrog wrote: post #62
thomasahle wrote: post #60

It took Andrew Wiles 7 years of intense work to solve Fermat's Last Theorem. The METR institute predicts that the length of tasks AI agents can complete doubles every 7 months. We should expect it to take until 2033 before AI solves Clay Institute-level problems with 50% reliability.

That's exactly why the Millennium Prize Problem Bench[1] was created. 1. https://mppbench.com/

That's amazing :D

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

#120

Post by threethirtytwo »

mkl wrote: post #40
ComplexSystems wrote: post #37

Earlier quoted context omitted.

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

Narrow AI? I’m not saying it’s AGI but this is not a narrow AI it’s a general AI given a narrow problem. ChatGPT.
Post reply on HN