I would sure be convinced by a Coq proof I couldn't understand. Professional mathematicians will face that kind of result eventually, if we keep progressing.