News for hackers. Stuff that matters.

A comment on AI solves IMO problems at silver medal level. Parent comment

Re:AI solves IMO problems at silver medal level by Smaug123 on Thursday July 25, 2024 @12:22PM (#41070461)
I think you might be thinking of the recent project to start Fermat's Last Theorem? The Riemann hypothesis has been easy to state (given what's in Mathlib) for years.
[ Parent | on HN ]
Re:AI solves IMO problems at silver medal level by Davidzheng on Thursday July 25, 2024 @01:39PM (#41071276)
Yeah lol i don't think either is hard to formalize in lean
[ Parent | on HN ]
Re:AI solves IMO problems at silver medal level by raincole on Thursday July 25, 2024 @04:03PM (#41072764)
They're not just formalizing Fermant's Last Theorem's statement itself. They're formalizing the proof.
[ Parent | on HN ]