what is a valid mathematical proof?

Question

from what i have seen in my experience with math we can say that

a valid proof is one that uses some form of logic (usually predicate logic) and uses logical rules of deduction and axioms or theorems in it's specific field to drive some new sentences that will eventually lead to the proposition we want to prove .

but we know that most of the proofs given in most of the fields (if not all!) are actually in informal language .

if we accept the definition above then non of these proofs are valid proofs .

how can we extend or change the idea of a valid proof to get to a better definition of a valid mathematical proof ?

Answer 1

We don't need to change, neither extend the idea of a mathematical proof just because many fields uses informal language. This is true that informal language might be more clear to the wide majority of people, but such a language can only be used for an explanation of the idea of the proof. On the other side the formal language is understood by a very small group of mathematicians. While, informal language allows a "bug" in a proof which can be ambiguously understood and lead to a false proofs, this cannot happen with a rigorous mathematical proof. A mistake in a rigorous proof sometimes can be found only by a well trained\experienced specialist of the particular field. This make the life not as simple as we wish, but this is the price we have to pay. I believe that stepping away from a formal\rigorous mathematical proof won't lead to anything good, but ambiguity.

Answer 2

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
• mathematicians
• physicists
• 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.

Answer 3

What you defined could be called a valid formal proof.

A valid mathematical proof (or a proof accepted by the mathematical community) on the other hand might be described as an informal(!) arrangement of arguments that the reader finds convincing in the sense that he or she strongly believes that it is possible to write down a valid formal proof reflecting the given arguments.

Some clarifying remarks:

• "A computer program tested all even integers from $4$ up to $10^{100}$ and verified that each of them can be written as sum of two primes" - This is not convincing enough to be a mathematical proof. It may be convincing enough to accept that the claim is correct for evens up to $10^{100}$ insofar as the computational steps of the program (once verified to be algorithmically correct) could be translated into a formal proof. But there is no hint as to how the argument might be converted to a general formal proof (by induction, say)

• A lengthy sequence of statements without explanation or comment and the mere claim that each line somehow follows from some of the preceeding lines (i.e., a formal proof) may not be lightheartedly accepted as mathematical proof. Indeed, the very lack of motivation and comment and helpful hints makes such a beast suspicious: One would really have to verify every single line and check that there are some preceeding lines leading to it; there is no such thing as diagonal reading. In fact, you may find a number of questions on this site where someone presents a proof of $1=0$ or the like consisting completely of commentless equations - and one has to really check that there is a step somewhere where the apparent transformation is a division by an expression that cannot be assumed to be non-zero. (Such a mistake is probably much easier to spot if at least some comments a la "Now I divide both sides by ..." are added)

• It may happen that some people are easier convinced than others, too easy sometimes, i.e., it may happen that an argument is accepted by some and for quite some time until it is discovered that there really is a gap. Maybe this is the risk of the lax notion of proof as formulated above. As mathematics is usually very proud of its rigor and undoubtable proofs, this possibility is often neglected or even mentally denied. But as a whole, such errors are very rare and in fact works claiming to prove a very significant result are generally subject to extreme scrutiny over some length of time until they are accepted (such as Wiles' proof of a theorem having Fermat's Last Theorem as corollary).

• If one really demands formal proofs, it takes considerably long to achieve meaningful results (e.g., Principia Mathematica has a proof of $1+1=2$ only somewhere in the middle of volume 2).

• There are ongoing projects to explicitly translate several important results from informal to formal. It may even happen that these projects hit on a few minor (and resolvable) gaps, but it is generally doubted that they may find real obstacles. And while I personally would find it significantly convincing for the proven result if such a computer-verifiable translation succeeds - the "real" proof is still the informal original ...

Answer 4

Here is Doron Zeilberger's opinion bearing on this topic with a pointer to some feedback from me (which includes some remarks on Hagen's point about Principia Mathematica).

Answer 5

First of all the distinction is not as important as one would think. When you use an informal formulation it can be considered a short hand description of how you would go about in creating the formal proof - just like a recipe for gingerbread is not a gingerbread, but it allows anyone to produce gingerbread if they're interested in doing so. Note that sharing proof is a matter of transferring knowledge of the proof to a receiver and if the receiver is convinced that he can produce a formal proof, actually produce a formal proof or is convinced that the proof is good enough - then it is good enough.

Second the informal language might look just like an informal language, but there's nothing that prevents a formal system to look just like some resemblance of a natural language. You could "simply" create a bijective map between a subset of the natural language and that of the formal system. Then what looks like a informal proof could be an image of a formal proof or even a formal proof itself.