News for hackers. Stuff that matters.

A comment on "Erdos problem #728 was solved more or less autonomously by AI". Parent comment

Re:"Erdos problem #728 was solved more or less autonomously ... by maxwells-daemon on Friday January 09, 2026 @09:02PM (#46562018)
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.

[ Parent | on HN ]
Re:"Erdos problem #728 was solved more or less autonomously ... by jjmarr on Saturday January 10, 2026 @02:07AM (#46563503)
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?

[ Parent | on HN ]
Re:"Erdos problem #728 was solved more or less autonomously ... by runeblaze on Saturday January 10, 2026 @09:09PM (#46572065)
Is it though? There is a reason gpt has codex variants. RL on a specific task raises the performance on that task
[ Parent | on HN ]
Re:"Erdos problem #728 was solved more or less autonomously ... by jjmarr on Saturday January 10, 2026 @09:30PM (#46572161)
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.
[ Parent | on HN ]
Re:"Erdos problem #728 was solved more or less autonomously ... by runeblaze on Sunday January 11, 2026 @12:35PM (#46577700)
Resouce-affording, if you are chasing the frontier of some more niche task you redo your training regime on the new-gen LLMs
[ Parent | on HN ]
Re:"Erdos problem #728 was solved more or less autonomously ... by Davidzheng on Saturday January 10, 2026 @03:20AM (#46563849)
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?
[ Parent | on HN ]