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.