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

191–200 of 385 posts

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

#191

Post by zamadatix »

tachim wrote: post #113
dang wrote: post #75

Earlier quoted context omitted.

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?

Absolutely, you've made something new you want to show us that we can try out. dang once posted some tips about making these types of submissions https://news.ycombinator.com/item?id=22336638 I'd recommend reading first though.

Edit: Also https://hn.algolia.com/?dateRange=all&page=2&prefix=true&que... for the most popular Show HNs. Don't be discouraged we like personal/open source projects most often, Obsidian made #1

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

#192

Post by charcircuit »

semi-extrinsic wrote: post #69
kridsdale3 wrote: post #22

Earlier quoted context omitted.

Not just for math, but ALL of Science suffers heavily from a problem of less than 1% of the published works being capable of being read by leading researchers. Google Scholar was a huge step forward for doing meta-analysis vs a physical library. But agents scanning the vastness of PDFs to find correlations and insights that are far beyond human context-capacity will I hope find a lot of knowledge that we have technic…

This idea is just ridiculous to anyone who's worked in academia. The theory is nice, but academic publishing is currently in the late stages of a huge death spiral. In any given scientific niche, there is a huge amount of tribal knowledge that never gets written down anywhere, just passed on from one grad student to the rest of the group, and from there spreads by percolation in the tiny niche. And papers are never h…

The same could be said about programmers, but we have adapted and started writing it all down so that AI cab use it.

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

#193

Post by johncolanduoni »

mjevans wrote: post #173
sibrahim wrote: post #158

Earlier quoted context omitted.

That's what's covered by the "assuming you have formalized the statement correctly" parenthetical. Given a formal statement of what you want, Lean can validate that the steps in a (tedious) machine-readable purported proof are valid and imply the result from accepted axioms. This is not AI, but a tiny, well reviewed kernel that only accepts correct formal logic arguments. So, if you have a formal statement that you'v…

I think the question is, how can humans have verification that the problem statement was correctly encoded into that Lean specification?

They can read the statement, and the definitions that the statement references. If everything it references is in a well-tread part of the Lean library, you can have pretty high confidence in a few minutes of going over the syntax.

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

#194

Post by dang »

minimaxir wrote: post #110
dang wrote: post #98

Earlier quoted context omitted.

Cynical, curmudgeonly, dismissive comments that ruin it as a place for curiosity. If you're interested, https://news.ycombinator.com/item?id=46515507 and https://news.ycombinator.com/item?id=46508115 are other places I wrote about this recently. It's the biggest problem facing HN, in my opinion.

> It's the biggest problem facing HN, in my opinion. Surprisingly the latest increase in polarization around generative AI has impacted Hacker News the least our of all tech social spaces.

I respect your awareness of that, which I'm sure is much broader than mine is. HN consumes my attention; I'm all depth and no breadth.

What I'm interested in is how well HN does at fulfilling its own mandate in its own terms. On that scale, it's getting worse—in this respect, at least, which is a big one. We're going to do something about it, the same way we've always tried to stave off the decline of this place (https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...).

If you're right that the phenomenon is affecting other places even more than HN then I guess we get to be the-worst-internet-forum-except-for-all-the-others even more than before (https://news.ycombinator.com/item?id=13494318, https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...) - not a bad outcome for HN, though I think it might be overly optimistic.

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

#195

Post by qnleigh »

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…

> If the proof is correct, Aristotle has a good chance at translating it into Lean

How does this depend on the area of mathematics of the proof? I was under the impression that it was still difficult to formalize most research areas, even for a human. How close is Aristotle to this frontier?

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

#196

Post by NewsaHackO »

D-Machine wrote: post #3

This is great, there is still so much potential in AI once we move beyond LLMs to specialized approaches like this. EDIT: Look at all the people below just reacting to the headline and clearly not reading the posts. Aristotle ( https://arxiv.org/abs/2510.01346 ) is key here folks. EDIT2: It is clear much of the people below don't even understand basic terminology. Something being a transformer doesn't make it an LLM…

> It is clear much of the people below don't even understand basic terminology. Something being a transformer doesn't make it an LLM (vision transformers, anyone) and if you aren't training on language (e.g. AlphaFold, or Aristotle on LEAN stuff), it isn't a "language" model.

I think it's because it comes off as you are saying that we should move off of GenAI, and alot of people use LLM when they mean GenAI.

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

#197

Post by NooneAtAll3 »

D-Machine wrote: post #76
MyFirstSass wrote: post #64

Based on Tao’s description of how the proof came about - a human is taking results backwards and forwards between two separate AI tools and using an AI tool to fill in gaps the human found? I don’t think it can really be said to have occurred autonomously then? Looks more like a 50/50 partnership with a super expert human one the one side which makes this way more vague in my opinion - and in line with my own AI test…

You're understanding correctly, this is back and forth between Aristotle and ChatGPT and a (very smart) user.

https://www.erdosproblems.com/forum/thread/728#post-2808

> There seems to be some confusion on this so let me clear this up. No, after the model gave its original response, I then proceeded to ask it if it could solve the problem with C=k/logN arbitrarily large. It then identified for itself what both I and Tao noticed about it throwing away k!, and subsequently repaired its proof. I did not need to provide that observation.

so it was literally "yo, your proof is weak!" - "naah, watch this! [proceeds to give full proof all on its own]"

I'd say that counts

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

#198

Post by svat »

tachim wrote: post #8

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

- Minor nit: The documentation mentions "uvx aristotlelib@latest aristotle" but that doesn't work; it should be "uvx --from aristotlelib@latest aristotle"

- It took me a minute or two of clicking around to figure out that the (only?) way to use it is to create an API key, then start aristotle in the terminal and interact with it there. It could be more obvious I think.

- Your profile links to http://www.cs.stanford.edu/~tachim/ which doesn't work; should be http://cs.stanford.edu/~tachim/ (without the www) (I think Stanford broke something recently for the former not to work.)

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

#199

Post by threethirtytwo »

gf000 wrote: post #136
threethirtytwo wrote: post #120

Earlier quoted context omitted.

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.

In a very specialized setup, in tandem with a verifier. Just because a specialized human placed in an F-16 can fly at Mach 2.0, doesn't mean humans in general can fly.

An apt analogy. A human is a general intelligence that can fly with an F-16.

What happens when we put an artificial general intelligence in an F-16? That's what happened here with this proof.

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

#200

Post by anthem2025 »

MyFirstSass wrote: post #87
D-Machine wrote: post #76

Earlier quoted context omitted.

You're understanding correctly, this is back and forth between Aristotle and ChatGPT and a (very smart) user.

I'm not sure i understand the wild hype here in this thread then. Seems exactly like the tests at my company where even frontier models are revealed to be very expensive rubber ducks, but completely fails with non experts or anything novel or math heavy. Ie. they mirror the intellect of the user but give you big dopamine hits that'll lead you astray.

[dead]
Post reply on HN