Hyper Tree Proof Search (Meta's math model from May 2022 (which they released some press about in November)) solved 10 IMO problems. Will we see a 5x improvement within one year?
Obviously the IMO problems must not be part of the training dataset.
1,000🏅 Top traders
| # | Name | Total profit |
|---|---|---|
| 1 | Ṁ506 | |
| 2 | Ṁ359 | |
| 3 | Ṁ326 | |
| 4 | Ṁ299 | |
| 5 | Ṁ148 |
People are also trading
Very unlucky. https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/ tests on post-2000 problems and solved 24 out of 30.
Given that a) 1959-1999 IMOs are generally easier than the newer ones; b) they do not train on any existing data at all; there is very little doubt this would have solved 50+ if they had just bothered to formalize the 40+ eligible problems from earlier IMOs.
.
@vluzko will the AI be required to examine the natural language statement of the problems, or does an AI that works on pre-formalized problems count?
@vluzko Wait, no, sorry, confused this question with a different one. For this one I'm using the same criteria as for HTPS, so pre-formalized problems are fine.
