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

351–360 of 385 posts

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

#351

Post by NetMageSCW »

maxwells-daemon wrote: post #157
pvillano wrote: post #133

Earlier quoted context omitted.

Is anyone working on applying these techniques to formal verification of software? My limited understanding of Rust is that it applies a fixed set of rules to guarantee memory safety. The rules are somewhat simple and limiting, for ease of understanding and implementation, but also because of undecidability. Programmers run into situations where they know that their code won't cause memory errors, but it doesn't foll…

We are! We very recently announced some results on formally proving the correctness of programs: https://harmonic.fun/news#blog-post-verina-bench-sota Formal methods are cool because, by contrast to tools like the borrow checker, you can prove some very "nonlocal" properties: this system does not deadlock, or it makes progress at least every N steps, etc.

How is “this system doesn’t deadlock” not the same as the halting problem?

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

#352

Post by oytis »

leggothrow wrote: post #46

This almost implies mathematicians aren’t some ungodly geniuses if something as absolutely dumb as an LLM can solve these problems via blind pattern matching. Meanwhile I can’t get Claude code to fix its own shit to save my life.

As I understand, a lot of mathematics, at least the part about solving problems, is basically back and forth between exploration (which involves pattern matching) and formalising. We've basically solved formalising a while ago, and now LLMs are getting better and better at exploration.

If you think about it, it's also what a lot of other intellectual activity looks like, at least in STEM.

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

#353

Post by jiggawatts »

jacquesm wrote: post #323
Mawr wrote: post #312

Earlier quoted context omitted.

Sure they, do, the problem makes no sense as stated. The solution to the stated problem is to remove all weights all at once, solved. Or even two at a time, opposite the centre of gravity. Solved, but not what you're asking I assume? You didn't even label your ASCII art, so I've no clue what you mean, are the bars at the end the supports or weights? Can I only remove one weight at a time? Initially I assumed you mean…

And yet, two people have solved it independently, so apparently it is adequately specified for some.

“Luck is not a strategy.”

I can successfully interpret total gibberish sometimes, but that’s not a robust approach even with humans let alone machines.

People have wildly different experiences utilising AI because of their own idiosyncrasies more than issues with the tools themselves.

It was pointed out by multiple groups (such as Anthropic) that their tools do a lot better with well organised codebases that are liberally commented.

I’ve worked on codebases where the AIs are just… lost. So are people!

Sure, some people can navigate the spaghetti… sometimes… but the success rate of changes is much lower.

Occasional success is not proof of correctness of approach. Consistent success is.

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

#354

Post by exe34 »

NetMageSCW wrote: post #349
exe34 wrote: post #289

Earlier quoted context omitted.

the argument here is that: 1. you write a proof in English that there is an infinite number of primes. 2. the llm writes 2+2=4 in lean. 3. lean confirms that this is correct and it's impossible that this proof is wrong.

You missed a whole section - a person creates a Lean formalization of #1 and Lean promptly says the AI proof is wrong because it doesn’t prove that formal problem statement. The question is in the person (or AI) creating the formal problem statement - how do you know it represents the problem the proof is supposed to be for? And the answer is for people in the field, in this case, formalizing the problem and verifyin…

I thought that's what I was trying to express between lines 1 and 2 above, but I may have failed to get it across. my understanding is that the danger is that the llm will create a proof that is correct but isn't about what the person thinks he's proving?

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

#355

Post by mkl »

threethirtytwo wrote: post #317
mkl wrote: post #259

Earlier quoted context omitted.

Not really. A completely unintelligent autopilot can fly an F-16. You cannot assume general intelligence from scaffolded tool-using success in a single narrow area.

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.

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

#356

Post by robot-wrangler »

frozenseven wrote: post #299
robot-wrangler wrote: post #178

Earlier quoted context omitted.

> Then what sort of math problem would be a milestone for you where an AI was doing something novel? What? If we're discussing novel synthesis, and it's being contrasted with answer-from-search / answer-from-remix.. the problem does not matter. Only the answer and the originality of the approach. Connecting two fields that were not previously connected is novel, or applying a new kind of technique to an old problem.…

If you squint hard enough, every new thing is an example of " answer-from-search / answer-from-remix ". Solving any Erdős problem in this manner was largely seen as unthinkable just a year ago. >the problem does not matter. Really? All of the other Erdős problems? Millennium Problems? Anything at all? This gets us directly into the territory of "nothing can convince us otherwise".

Tiresome. You're quoting me out of context, and generally assigning me the POV you want to argue with. You come across as pro-AI looking for anti-AI to do combat with. First, I'm not the right guy, and second, all I'm really saying above is that if we're going to do argument-from-authority, maybe let's engage with what the authority is actually saying in TFA.

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

#357

Post by wizzwizz4 »

NetMageSCW wrote: post #350
wizzwizz4 wrote: post #316

Earlier quoted context omitted.

This problem was even worse: it's matched by the formal grammar, but the naïve formalisation has a trivial answer, so it is clearly not what was intended.

That clearly may be doing some heavy lifting. It is assumed that trivial answer wasn’t what was intended for the problem, but unless someone asked Erdos, I don’t think we know.

Considering that he did some work towards the problem, tackling non-trivial cases, I think we do know. There's no way he wouldn't have perceived trivial solutions at some point.

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

#358

Post by frozenseven »

robot-wrangler wrote: post #356
frozenseven wrote: post #299

Earlier quoted context omitted.

If you squint hard enough, every new thing is an example of " answer-from-search / answer-from-remix ". Solving any Erdős problem in this manner was largely seen as unthinkable just a year ago. >the problem does not matter. Really? All of the other Erdős problems? Millennium Problems? Anything at all? This gets us directly into the territory of "nothing can convince us otherwise".

Tiresome. You're quoting me out of context, and generally assigning me the POV you want to argue with. You come across as pro-AI looking for anti-AI to do combat with. First, I'm not the right guy, and second, all I'm really saying above is that if we're going to do argument-from-authority, maybe let's engage with what the authority is actually saying in TFA.

I don't think I quoted you out of context. In any case, Terence Tao and co. are doing wonderful work in this area. I'd encourage everyone to bookmark the following link: https://github.com/teorth/erdosproblems/wiki/AI-contribution...

It's a rapidly evolving story and I expect H1 2026 to bring much clarity on this topic. Especially with upcoming model releases and more professional mathematicians taking an interest.

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

#359

Post by frozenseven »

DiscourseFan wrote: post #321
frozenseven wrote: post #295

Earlier quoted context omitted.

>AGI advocates treat machine intelligence like some sort of God that will smite non-believers and reward the faithful. >The real world is not composed of rewards and punishments. Most "AGI advocates" say that AGI is coming, sooner rather than later, and it will fundamentally reshape our world. On its own that's purely descriptive. In my experience, most of the alleged "smiting" comes from the skeptics simply being wr…

You should look into “Roko’s Basilisic,” its a genuine belief that often goes alongside that of AGI.

I should be the target audience for this stuff, but I honestly can't name a single person who believes in this "Roko's basilisk" thing. To my knowledge, even the original author abandoned it. There probably are a small handful out there, but I've never seen 'em myself.

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

#360

Post by runeblaze »

jjmarr wrote: post #231
maxwells-daemon wrote: post #169

Earlier quoted context omitted.

Aristotle's output is formally verified in Lean, so you can run it for days on a hard problem and be assured that the answer, no matter how complex, is right without needing to manually check it. Claude Code can write lean, but we do a heck of a lot of RL on theorem proving, so Aristotle winds up being much better at writing Lean than other coding agents are.

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 reply on HN