This question resolves when an AI first gets IMO Gold. It resolves YES if this AI uses formal methods in some way, as opposed to an informal-to-informal approach.
For example, an AI as described in the paper "HyperTree Proof Search for Neural Theorem Proving" would satisfy this condition, whereas Minerva would not.
Related questions
@FlorisvanDoorn I'm going for the definition which is being used by the big 2025 market (which is admittedly a little underspecified itself). What's clearly specified about that market is that there must be a computer system built before an IMO which gets scores gold on that IMO. As for who scores the test and whether the questions are processed into a formal format before being fed to the machine is unclear - I will try to match whatever criteria that market uses. At the very least if the system is entirely NLP based and outputs an obviously correct proof for each of the questions in English, then this could resolve NO.
@BoltonBailey Actually, looking at what Paul Christiano has said in the comment for that market, it seems like he would accept either formal or informal inputs, so I will likely accept the same here.