AI solves IMO problems at silver medal level

Re:AI solves IMO problems at silver medal level by Ericson2314 on Thursday July 25, 2024 @12:05PM (#41070255)

They're def gonna go after the Riemann hypothesis with this, hehe.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by nwoli on Thursday July 25, 2024 @12:18PM (#41070430)

Guessing the context here is that the RH was recently translated into Lean. Would be very cool if they threw their compute on that

[ Parent | on HN ]

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 ]