I think math is so tractable because of lean only. If there were an automated test to determine if their claim was true, it could just generate a thousand claims in the right direction until it hits.