https://news.ycombinator.com/item?id=46550836
Another view on that.
“Erdos problem #728 was solved more or less autonomously by AI”
241–250 of 385 posts
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#242Earlier quoted context omitted.
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.
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…
Lean is doing logical AI, the classical AI part.
Aristotle is doing the matching AI part, the modern LLM approach, previously called fuzzy logic.
Both are AI.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#243Earlier quoted context omitted.
> Any talk of "AGI" is, as always, ridiculous. How did you arrive at "ridiculous"? What we're seeing here is incredible progress over what we had a year ago. Even ARC-AGI-2 is now at over 50%. Given that this sort of process is also being applied to AI development itself, it's really not clear to me that humans would be a valuable component in knowledge work for much longer.
It requires constant feedback, critical evaluation, and checks. This is not AGI, its cognitive augmentation. One that is collective, one that will accelerate human abilities far beyond what the academic establishment is currently capable of, but that is still fundamentally organic. I don't see a problem with this--AGI advocates treat machine intelligence like some sort of God that will smite non-believers and reward…
It does seem that the venn diagram of "roko's basilisk" believers and "AGI is coming within our lifetimes" believers is nearly a circle. Would be nice if there were some less... religious... arguments for AGI's imminence.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#244This 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.
Ugh, you're right. This was not intended. Conflating LLMs with GenAI is a serious error, but you're right, it is obviously a far more common error than I realized. I clearly should have said "move beyond solely LLMs" or "move beyond LLMs in isolation", perhaps this would have avoided the confusion.
This is a really hopeful result for GenAI (fitting deep models tuned by gradient descent on large amounts of data), and IMO this is possible because of specific domain knowledge and approaches that aren't there in the usual LLM approaches.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#2452026 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.
[deleted]
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#246Earlier quoted context omitted.
What are the benefits of Aristotle over a general-purpose coding assistant like Claude Code?
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.
how strong is your internal informal LLM at theorem-proving before the formalization stage? or it's combined in a way so that is not measurable?
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#247Earlier quoted context omitted.
I think the question is, how can humans have verification that the problem statement was correctly encoded into that Lean specification?
Isn't that kind of a general problem with proofs, even when they're written by humans? There's nothing stopping someone from accidentally writing their own Lean proof that has slightly different semantics than an English version of the same proof, or even for their English proof to subtly miss something important or make an incorrect logical leap. This seems like a bit of a double standard, although maybe there's nua…
One nuance you are missing is that the discussion is about formalizing the statement (the theorem), not the proof. The latter is what the article is about, but that doesn't suffice if you can't trust that the statement is also correctly formalized.
These are the two main problems:
1. Formalizing a theorem.
2. Finding a formal proof.
Part 2 is where AI could help as proof search is full of heuristics. That's also how humans find proofs and is one of the main skills of a mathematician. The formal proof can then be machine checked with well known and mature techniques not involving AI.
Part 1 is the part that's missing and will always be hard. It's also the issue with formal verification of programs for which correctness criteria are often very complex and it's easy to mess up the formalization, so that even if you trust the proof, you can't trust that it proves the right thing.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#248When Deep Blue beat Kaspaorov, it was not the end of career for human players. But since mathematics is not a sport with human players, what are the career prospects for mathematicians or mathematics-like fields?
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#249Earlier 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…
Lean is doing logical AI, the classical AI part. Aristotle is doing the matching AI part, the modern LLM approach, previously called fuzzy logic. Both are AI.
Calling Lean "AI" is quite a stretch. Though I'm also in the camp that dislikes the inflationary use of "AI" for LLMs, so I have sympathies for your viewpoint.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#250Earlier quoted context omitted.
It requires constant feedback, critical evaluation, and checks. This is not AGI, its cognitive augmentation. One that is collective, one that will accelerate human abilities far beyond what the academic establishment is currently capable of, but that is still fundamentally organic. I don't see a problem with this--AGI advocates treat machine intelligence like some sort of God that will smite non-believers and reward…
It does seem that the venn diagram of "roko's basilisk" believers and "AGI is coming within our lifetimes" believers is nearly a circle. Would be nice if there were some less... religious... arguments for AGI's imminence.
I think the “Roko’s Basilisk” thing is mostly a way for readers of Nick Land to explain part of his philosophical perspective without the need for, say, an actual background in philosphy. But the simplicity reduces his nuanced thought into a call for a sheeplike herd—they don’t even need a shepherd! Or perhaps there is, but he is always yet to come…best to stay in line anyway, he might be just around the corner.