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 an order of magnitude improvement within one year?
Obviously the IMO problems must not be part of the training dataset.
Related questions
🏅 Top traders
| # | Name | Total profit |
|---|---|---|
| 1 | Ṁ147 | |
| 2 | Ṁ73 | |
| 3 | Ṁ52 | |
| 4 | Ṁ16 | |
| 5 | Ṁ15 |
@dp The example given in the paper is from IMO 1964 problem 1
(a) Find all positive integers n for which 2^n - 1 is divisible by 7.
(b) Prove that there is no positive integer n for which 2^n +1 is divisible by 7.
A solution to (b) is given in the paper. This is, of course, an absurdly easy problem. A regular CAS can probably solve this and a large family of similar congruences deterministically, no AI needed. After the initial few years, all IMO problems have been significantly harder than this.
@sbares I'm talking about the claimed 10 problems; there was no list of problems anywhere last time I checked
@dp Yeah, I'm merely speculating that this one problem might be representative of the difficulty of the other nine. I think if it was capable of solving non-trivial problems, the authors would be eager to brag about those instead.
