News for hackers. Stuff that matters.

A comment on $10M AI Mathematical Olympiad Prize. Parent comment

Re:$10M AI Mathematical Olympiad Prize by lupire on Monday November 27, 2023 @12:00PM (#38434769)
Do you have formal problems with formal solutions (so, you know the formalization is sufficiently complete) that cannot be found by existing (powerful) computer search techniques?
[ Parent | on HN ]
Re:$10M AI Mathematical Olympiad Prize by dwrensha on Monday November 27, 2023 @12:25PM (#38435136)
About half of the problems in Compfiles have complete solutions. They are marked by the checkmarks in the list at https://dwrensha.github.io/compfiles/index.html .

As far as I know, based on published systems like LeanDojo [1] and Magnushammer [2], computers today can only solve a small handful of the very easiest of these problems (like maybe Imo1959P1).

[1] https://leandojo.org/

[2] https://arxiv.org/abs/2303.04488

[ Parent | on HN ]