My personal opinion goes more along:
A proof is valid if it convinces a significant number of experts in
the field to declare it valid.
A prime example was Andrew Wiles proof of FLT, a long and complicated proof, with initial flaws as well, in a subject only a few were deep into.
A PhD student in algebra told me at that time that he would need two years of preparation to start understanding it. It seems that less than 50 people were able to judge that proof when it came out. So maybe 20 folks did do the work and said they think it is ok. Is such a proof valid? :-)
Then we might compare the early pioneers of calculus, the likes of the Bernoullis, Euler, Leibniz and Newton with the latter more critical ones like Cauchy and Weierstrass. The latter group seem to have desired more rigour than the first group. A proof that was good enough for the first group was probably not good enough for the second group some hundred years later.
So a proof is at best valid for a certain group who is confident to understand it and reflects the opinion of that group that it is sufficient.
If we present a proof to various groups, e.g.
- some folks on the street
- your neighbours
- high school students
- republican U.S. presidential candidates, like Donald Trump or Dr. Ben Carson
- experts in the field
- ancient or modern scientists
whose opinion should we trust to be most likely in accordance with the mathematical truth (deciding if the proof proofs its claim or not)?
Conventional wisdom is to go with the established experts, who can be wrong of course too.
About "informal language" vs "formal language":
To use which language and abstraction level should be guided by how helpful it is for the job to describe and solve the problem at hand.
A mathematician's brain might better operate on informal language combined with formal language while a machine, running the software of a theorem checker (e.g. Coq), has, at the present state of the art, only the choice to be fed with formal language.
Both planes of description and operation have their advantages or disadvantages, I see both as complementing each other. I would not say that a formal proof is better per se, it is harder to create, understand and prone to errors as well. Of course it can make use of the incredible speed, accuracy and memory of a modern machine.