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

211–220 of 385 posts

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

#211

Post by rtpg »

aidenn0 wrote: post #148
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.

I feel like even outside of AI translation, formalization not capturing the spirit of what the informal description was provided is always a risk.

This is also a big risk when trying to prove code correctness: "prove this algo works" means you gotta define "works" along certain axes, and if you're very unlucky you might have a proof that exploits the uncertainty around a certain axis.

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

#212

Post by mkehrt »

aidenn0 wrote: post #208
mrtesthah wrote: post #177

Earlier quoted context omitted.

They probably need to be able to read and understand the lean language.

I can read and understand e.g. Python, but I have seen subtle bugs that were hard to spot in code generated by AI. At least the last time I tried coding agents (mid 2025), it was often easier to write the code myself then play "spot the bug" with whatever was generated. I don't know anything about Lean, so I was wondering if there were similar pitfalls here.

In this case the human written statement of the theorem is small. Can there be bugs? Absolutely! But it's essentially a few lines of code worth of thinking.

The lean proof checker then checks to make sure the proof actually proves the statement.

In this case an AI is generating the proof, but if it "compiles" it's correct. The only thing humans need to check is the statement to be proven.

(I don't know anything about this project but I've played around with lean and used other proof checkers more sesrisously).

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

#213

Post by hyperadvanced »

lwansbrough wrote: post #14

Can anyone with specific knowledge in a sophisticated/complex field such as physics or math tell me: do you regularly talk to AI models? Do feel like there's anything to learn? As a programmer, I can come to the AI with a problem and it can come up with a few different solutions, some I may have thought about, some not. Are you getting the same value in your work, in your field?

I’m a hobbyist math guy (with a math degree) and LLMs can at least talk a little talk or entertain random attempts at proofs I make. In general they rebuke my more wild attempts, and will lead me to well-trodden answers for solved problems. I generally enjoy (as a hobby) finding fun or surprising solutions to basic problems more than solving novel maths, so LLMs are fun for me.

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

#214

Post by eru »

zozbot234 wrote: post #161
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…

Formal verification of program correctness is also (for obvious reasons) key to unlocking AI-driven synthesis (i.e. 'vibe' coding) of "correct" programs that will verifiably meet the given spec.

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.

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

#215

Post by abdullahkhalids »

sothatsit wrote: post #187
abdullahkhalids wrote: post #31

Earlier quoted context omitted.

I work in quantum computing. There is quite a lot of material about quantum computing out there that these LLMs must have been trained on. I have tried a few different ones, but they all start spouting nonsense about anything that is not super basic. But maybe that is just me. I have read some of Terence Tao's transcripts, and the questions he asks LLMs are higher complexity than what I ask. Yet, he often gets reason…

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.

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

#216

Post by fc417fc802 »

ACS_Solver wrote: post #151
epolanski wrote: post #42

Earlier quoted context omitted.

AGI in its standard definition requires matching or surpassing humans on all cognitive tasks, not just in some, especially some where only handful of humans took a stab on.

Surely AGI would be matching humans on most tasks. To me, surpassing humans on all cognitive tasks sounds like superintelligence, while AGI "only" need to perform most, but not necessarily all, cognitive tasks at the level of a human highly capable at that task.

Personally I could accept "most" provided that the failures were near misses as opposed to total face plants. I also wouldn't include "incompatible" tasks in the metric at all (but using that to game the metric can't be permitted either). For example the typical human only has so much working memory, so tasks which overwhelm that aren't "failed" so much as "incompatible". I'm not sure exactly what that looks like for ML but I expect the category will exist. A task that utilizes adversarial inputs might be an example of such.

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

#217

Post by dpacmittal »

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…

There's a lot more detail in this reddit post from the author - https://www.reddit.com/r/OpenAI/comments/1q6yw5g/how_we_used...

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

#218

Post by nateberkopec »

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…

>assuming you have formalized the statement correctly

That's a pretty big assumption, though, isn't it? As we saw the Navier-Stokes psychosis episode over the New Year holiday, formalizing correctly really isn't guaranteed.

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

#220

Post by maxbond »

dang wrote: post #194
minimaxir wrote: post #110

Earlier quoted context omitted.

> 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 ( ht…

> On that scale, it's getting worse...

I don't mean to express doubt (you would know better than I) but what makes you say that?

Do you think it's a consequence of external factors like the current political climate or of internal factors like HN getting larger?

Post reply on HN