Why would this be hard for the machines? A lot of math contest problems are about trying some rearrangements or substitutions, using a few principles to guide you towards the solution.
If you give the machine some equations, wouldn't it find a path to the solution pretty fast? Aren't there solvers that aren't considered AI that do that sort of thing?
I did some math contests in school, and a lot of the problems needed some brute force element along with a bit of overview so you didn't waste too much time. Often there'd be a problem that you'd look at and think "hmm this will solve via integration by parts" but the thing was complex enough that you'd potentially screw something up.
I looked in the Gitlab, it seems the problems are already encoded in Lean. Haven't you solved a major part of the problem already if you can formally encode it like that? Half the fun of math contests is getting over the WTF feeling.
If you give the machine some equations, wouldn't it find a path to the solution pretty fast? Aren't there solvers that aren't considered AI that do that sort of thing?
I did some math contests in school, and a lot of the problems needed some brute force element along with a bit of overview so you didn't waste too much time. Often there'd be a problem that you'd look at and think "hmm this will solve via integration by parts" but the thing was complex enough that you'd potentially screw something up.
I looked in the Gitlab, it seems the problems are already encoded in Lean. Haven't you solved a major part of the problem already if you can formally encode it like that? Half the fun of math contests is getting over the WTF feeling.