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

361–370 of 385 posts

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

#361

Post by threethirtytwo »

mkl wrote: post #355
threethirtytwo wrote: post #317

Earlier quoted context omitted.

I didn’t assume agi. I assumed extreme performance of a general AI matching and exceeding average human intelligence when placed in an F16 or an equivalent cockpit specified for conducting math proofs. That’s not agi at all. I don’t think you understand that LLMs will never hit agi even when they exceed human intelligence in all applicable domains. The main reason is they don’t feel emotions. Even if the definition o…

> I didn’t assume agi. You literally said: >>> What happens when we put an artificial general intelligence in an F-16? That's what happened here with this proof. You're claiming I said a lot of things I didn't; everything you seem to be stating about me in this comment is false.

That's called a hypothetical. I didn't say that we put an AGI into an F-16. I asked what the outcome would be. And the outcome is pretty similar. Please read carefully before making a false statement.

>You're claiming I said a lot of things I didn't; everything you seem to be stating about me in this comment is false.

Apologies. I thought you were being deliberate. What really happened is you made a mistake. Also I never said anything about you. Please read carefully.

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

#362

Post by jjmarr »

runeblaze wrote: post #360
jjmarr wrote: post #231

Earlier quoted context omitted.

Seeing a task-specific model be consistently better at anything is extremely surprising given rapid innovation in foundation models. Have you tried Aristotle on other, non-Lean tasks? Is it better at logical reasoning in general?

Is it though? There is a reason gpt has codex variants. RL on a specific task raises the performance on that task

Post-training doesn't transfer over when a new base model arrives so anyone who adopted a task-specific LLM gets burned when a new generational advance comes out.

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

#363

Post by oh_my_goodness »

NetMageSCW wrote: post #346
schrodinger wrote: post #336

Earlier quoted context omitted.

Voters: please reconsider your ups and downs. I think the “Are you an expert” question triggered a lot of downvotes when it was in fact asked in good faith to judge the person’s perspective of easy and hard.

And I would say there is no way to ask that question in good faith. (Tedious proof by cases left as an exercise for readers.) The correct question would have been, does anyone else agree with the statement. In this particular case, the amount knowledge needed (of e.g. Lean language, math and Erdos problems) means any credible statement about the difficulty requires an expert.

"Are you an expert?" is a perfectly respectful question.

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

#364

Post by eru »

f1shy wrote: post #228
eru wrote: post #214

Earlier quoted context omitted.

Not all aspects of a spec can be formally encoded. But even half-way houses are good. Eg you can give the vague spec 'build me a todo list app', but you can still formally prove that everything your app does finishes, or even that it finishes in reasonable time.

Yes. For sure we will never be able to 100% automate the whole SWE process. As you say, the first input is a human wish, and there comes the joke of the genie that always screw the wishes by leaving something obvious out, because not explicitly specified. Also I think at some point the halting problem will make some programs impossible to test. But it would so great, program in a loose syntax, but with more safety th…

> Also I think at some point the halting problem will make some programs impossible to test.

No, not at all. The halting problem isn't much of a problem here.

To elaborate: yes, it's pretty much impossible to decide whether an arbitrary programme will halt. But we aren't dealing with arbitrary programmes, you carefully have your agent craft programmes that are easy to prove correct.

There are languages available today whose type systems already only let you write terminating programmes. See eg https://news.ycombinator.com/item?id=32102203 the Dhall language. Or Agda or Lean itself (unless you specifically opt out via the 'partial' keyword. But it's trivial to check whether someone used 'partial'.)

If your agent write a programme that's not easy to prove to be terminating, you don't try harder to prove. You just flag that as an error and have the agent try again.

Just like as a human code reviewer you reject Pull Requests that are too complicated to understand: you don't even bother figuring out whether they are technically correct or not.

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

#365

Post by jiggawatts »

jacquesm wrote: post #304
ogogmad wrote: post #303

Earlier quoted context omitted.

The problem is unclear. I think you have a labelled graph G=(V, E) with labels c:V->R, such that each node in V consists of a triple (L, R, S) where L is a sequence of weights are on the left, R is a sequence of weights that are on the right, and S is a set of weight that have been taken off. Define c(L, R, S) to be the centre of mass. Introduce an undirected edge e={(L, R, S), (L', R', S')} between (L, R, S) and (L'…

You are overthinking it.

You are underspecifying it.

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

#366

Post by sothatsit »

abdullahkhalids wrote: post #215
sothatsit wrote: post #187

Earlier quoted context omitted.

This often feels like an annoying question to ask, but what models were you using? The difference between free ChatGPT, GPT-5.2 Thinking, and GPT-5.2 Pro is enormous for areas like logic and math. Often the answer to bad results is just to use a better model. Additionally, sometimes when I get bad results I just ask the question again with a slightly rephrased prompt. Often this is enough to nudge the models in the r…

I have openrouter account, so I try different models easily. I have tried Sonnet, Opus, various versions of GPT, Deepseek. There are certainly differences in the quality. I also do rephrase prompts all the time. But ultimately, I can't quite get them to work in quantum computing. Far easier to get them to answer coding or writing related questions.

Both Erdos #728 and #729 were solved with the use of GPT-5.2 Pro. Lesser models have much worse performance on difficult problems like these.

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

#368

Post by casey2 »

dang wrote: post #52
bgwalter wrote: post #21

[flagged]

We need you to stop posting shallow dismissals and cynical, curmudgeonly, and snarky comments. We asked you about this just recently, but it's still most of what you're posting. You're making the site worse by doing this, right at the point where it's most vulnerable these days. Your comment here is a shallow dismissal of exactly the type the HN guidelines ask users to avoid here: " Please don't post shallow dismissa…

I'd rather HN become a much worse place than the world suffer though AI massive wealth theft, the BIG LIE that will convince elites to kill millions of people.

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

#369

Post by ndriscoll »

oh_my_goodness wrote: post #328
ndriscoll wrote: post #179

Earlier quoted context omitted.

The problem statement is apparently > Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn? Which seems like it's the type of thing you give as a homework problem to state formally in an intro class.

Everyone has a different perspective, based on their math background. From the OP's perspective, the formalization of this problem statement was apparently worth talking about. On the other hand, for you it's just a homework problem that belongs in an intro class. Let's just be generous and try to accept these differences.

My comment was exactly about the required math background though. Anyone who's completed an intro to proof class would find that kind of statement easy to formalize because they would have had to write similar statements for homework. That provides some context: everyone who's interested in computer theorem provers probably has some experience with proofs, so formalizing that statement should be easy for them. i.e. (for this kind of problem) it's not really "the hard part" for people who are seriously working on this stuff.

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

#370

Post by ndriscoll »

NetMageSCW wrote: post #346
schrodinger wrote: post #336

Earlier quoted context omitted.

Voters: please reconsider your ups and downs. I think the “Are you an expert” question triggered a lot of downvotes when it was in fact asked in good faith to judge the person’s perspective of easy and hard.

And I would say there is no way to ask that question in good faith. (Tedious proof by cases left as an exercise for readers.) The correct question would have been, does anyone else agree with the statement. In this particular case, the amount knowledge needed (of e.g. Lean language, math and Erdos problems) means any credible statement about the difficulty requires an expert.

It doesn't require an expert though. That was kind of my point. If you've taken an intro proof class (so the intro class for math majors/the topic), and if you've fiddled with Lean a bit (e.g. played some of the Natural Numbers Game another commenter linked), you'll know it's easy (source: I did math in my undergrad, and have fiddled with Lean a bit). Honestly I expect intro proof classes will start to be centered around something like Lean soonish if some aren't already incorporating it, and we'll see math majors more explicitly making the connection between program and proof.

Like if someone were incredulous that we could reasonably analyze running time and memory usage of something like merge sort and I said that's a standard example in an intro algorithms course, presumably people would be like "yeah it is".

Post reply on HN