Will an AI smart enough to win math competitions be AGI?