Uncovering the Means to Verify Math Proofs

[solakis1]

I feel the question i am going to ask it is one of the most important question ,if not the most important,in Mathematics.
And i may add if answered correctly a lot of misunderstanding and useless arguing can be avoided.

So here is the question:

What are the mathematical means or theories that we have at our disposal for checking the correctness of a mathematical proof

 

[Evgeny.Makarov]

What are the mathematical means or theories that we have at our disposal for checking the correctness of a mathematical proof

Twentieth century mathematics, in particular, mathematical logic, provided a precise definition of a mathematical proof. So now, at least in theory, the question whether a given argument is a correct proof has a precise answer. Moreover, when the supposed proof is given in full detail, determining whether it is correct is relatively simple and can be done by a computer. This is in contrast to the problem of finding a proof, for which it has been proven that no single algorithm can exist.In practice, there are technical problems because a proof to be checked is rarely presented in full detail. In fact, even relatively detailed but sufficiently complicated paper proofs have pretty big gaps because they omit steps that are obvious to people. Writing complicated proofs in full detail has become possible only using computers. Currently there exist several programs (such as Coq and Isabelle), called interactive proof assistants, that incorporate definitions of a proof and allow users to interactively build proofs according to these definitions. They automatically perform routine steps, such as proving propositional tautologies or polynomial equations over a ring, allowing the user to focus on high-level steps. In the best proof develoments, the size of proof scripts that the user writes approaches the size of paper proofs.Out of significant proof evelopments one can point out the proof in Coq of four color theorem in 2005 by Georges Gonthier and Benjamin Werner. This theorem was first proved in 1976, and the proof required a lot of computation, so there were doubts regarding it. Just this September, Georges Gonthier and his team used Coq to formalize Feit–Thompson theorem, whose paper proof takes 255 pages. Thomas Hales is finishing the formalization of Kepler conjecture in HOL Light.Does this answer your question?

 

[solakis1]

Twentieth century mathematics, in particular, mathematical logic, provided a precise definition of a mathematical proof. So now, at least in theory, the question whether a given argument is a correct proof has a precise answer. Moreover, when the supposed proof is given in full detail, determining whether it is correct is relatively simple and can be done by a computer. This is in contrast to the problem of finding a proof, for which it has been proven that no single algorithm can exist.In practice, there are technical problems because a proof to be checked is rarely presented in full detail. In fact, even relatively detailed but sufficiently complicated paper proofs have pretty big gaps because they omit steps that are obvious to people. Writing complicated proofs in full detail has become possible only using computers. Currently there exist several programs (such as Coq and Isabelle), called interactive proof assistants, that incorporate definitions of a proof and allow users to interactively build proofs according to these definitions. They automatically perform routine steps, such as proving propositional tautologies or polynomial equations over a ring, allowing the user to focus on high-level steps. In the best proof develoments, the size of proof scripts that the user writes approaches the size of paper proofs.Out of significant proof evelopments one can point out the proof in Coq of four color theorem in 2005 by Georges Gonthier and Benjamin Werner. This theorem was first proved in 1976, and the proof required a lot of computation, so there were doubts regarding it. Just this September, Georges Gonthier and his team used Coq to formalize Feit–Thompson theorem, whose paper proof takes 255 pages. Thomas Hales is finishing the formalization of Kepler conjecture in HOL Light.Does this answer your question?

No ,you confused me even more.

But let us take things one at a time.

What do you mean by:

"Moreover, when the supposed proof is given in full detail "

Give an example if it is possible

 

[Evgeny.Makarov]

What do you mean by:

"Moreover, when the supposed proof is given in full detail "

Give an example if it is possible

Consider the following claim.

Proposition (Integer Root). Suppose $f:\mathbb{N}\to\mathbb{N}$ is unbounded, i.e., there exists a
function $g$ such that $f(g(z))>z$ for all $z$. If $f(0)\le y$, then there exists an integer root of the equation $f(x)-y=0$, i.e., there exists an $x$ such that $f(x)\le y<f(x+1)$.

Proof. Towards contradiction, suppose no such $x$ exists. We prove by induction on $x$ that $f(x)\le y$. The base case is given. For the induction step, assume that $f(x)\le y$. If $y<f(x+1)$, then we have a contradiction with our assumption, so $f(x+1)\le y$, which concludes the induction step. Putting $x=g(y)$ we get $f(g(y))\le y$, contradicting the assumption that $f(g(y))>y$.

The following is a formal proof in Fitch notation.

View attachment 507

The English proof above is rather detailed, so the formal proof has about the same size. In contrast, if the claim above were a part of a much more complicated proof, then it is likely that it would be dismissed as obvious.

Below is the statement of the theorem and its actual proof in the Coq proof assistant (the function S is the successor on natural numbers).

Theorem int_root : forall y, f 0 <= y -> exists x, f x <= y < f (S x).

fun (y : nat) (H1 : f 0 <= y) =>
NNPP (exists x : nat, f x <= y < f (S x))
  (fun H2 : ~ (exists x : nat, f x <= y < f (S x)) =>
   (fun H3 : forall x : nat, f x <= y =>
    le_not_lt (f (g y)) y (H3 (g y)) (f_unbounded y))
     (fun x : nat =>
      nat_ind (fun x0 : nat => f x0 <= y) H1
        (fun (x0 : nat) (IH : f x0 <= y) =>
         let o := le_or_lt (f (S x0)) y in
         match o with
         | or_introl H3 => H3
         | or_intror H3 =>
             False_ind (f (S x0) <= y)
               (H2
                  (ex_intro (fun x1 : nat => f x1 <= y < f (S x1)) x0
                     (conj IH H3)))
         end) x))

The proof is a written as a \(\lambda\)-term using a syntax close to the OCaml programming language. This proof contains all details (it relies on lemmas le_not_lt and le_or_lt, which were proved earlier). The computer has verified that it indeed proves the claim above according to the rules of mathematics programmed into Coq.

Unfortunately, the size of formal proofs and time required to write them is often significantly greater than the size and time associated with paper proofs. For example, pigeonhole principle is usually considered intuitively obvious and is rarely proved.

Proposition (Pigeonhole Principle). Suppose \(f:\mathbb{N}\to\mathbb{N}\) and \(n\ge 0\). If \(f(k)\le n\) for all \(0\le k\le n+1\), then there exist \(0\le k_1,k_2,\le n+1\) such that \(f(k_1)=f(k_2)\).

Formally, this statement is proved by induction on $n$. Further, from a formal proof it is possible to extract an algorithm that, given \(f\) and $n$, will find the required $k_1$ and $k_2$. That is, this algorithm is already implicitly contained in the proof. However, I would guess that for most people, writing such algorithm requires more thought that agreeing that the principle is true. This implies to me that formal proofs often contain details that authors of corresponding paper proofs don't think about.

 

[solakis1]

Consider the following claim.

Proposition (Integer Root). Suppose $f:\mathbb{N}\to\mathbb{N}$ is unbounded, i.e., there exists a
function $g$ such that $f(g(z))>z$ for all $z$. If $f(0)\le y$, then there exists an integer root of the equation $f(x)-y=0$, i.e., there exists an $x$ such that $f(x)\le y<f(x+1)$.

Proof. Towards contradiction, suppose no such $x$ exists. We prove by induction on $x$ that $f(x)\le y$. The base case is given. For the induction step, assume that $f(x)\le y$. If $y<f(x+1)$, then we have a contradiction with our assumption, so $f(x+1)\le y$, which concludes the induction step. Putting $x=g(y)$ we get $f(g(y))\le y$, contradicting the assumption that $f(g(y))>y$.

The following is a formal proof in Fitch notation.

View attachment 507

The English proof above is rather detailed, so the formal proof has about the same size. In contrast, if the claim above were a part of a much more complicated proof, then it is likely that it would be dismissed as obvious.

Below is the statement of the theorem and its actual proof in the Coq proof assistant (the function S is the successor on natural numbers).

Theorem int_root : forall y, f 0 <= y -> exists x, f x <= y < f (S x).

fun (y : nat) (H1 : f 0 <= y) =>
NNPP (exists x : nat, f x <= y < f (S x))
  (fun H2 : ~ (exists x : nat, f x <= y < f (S x)) =>
   (fun H3 : forall x : nat, f x <= y =>
    le_not_lt (f (g y)) y (H3 (g y)) (f_unbounded y))
     (fun x : nat =>
      nat_ind (fun x0 : nat => f x0 <= y) H1
        (fun (x0 : nat) (IH : f x0 <= y) =>
         let o := le_or_lt (f (S x0)) y in
         match o with
         | or_introl H3 => H3
         | or_intror H3 =>
             False_ind (f (S x0) <= y)
               (H2
                  (ex_intro (fun x1 : nat => f x1 <= y < f (S x1)) x0
                     (conj IH H3)))
         end) x))

The proof is a written as a \(\lambda\)-term using a syntax close to the OCaml programming language. This proof contains all details (it relies on lemmas le_not_lt and le_or_lt, which were proved earlier). The computer has verified that it indeed proves the claim above according to the rules of mathematics programmed into Coq.

Unfortunately, the size of formal proofs and time required to write them is often significantly greater than the size and time associated with paper proofs. For example, pigeonhole principle is usually considered intuitively obvious and is rarely proved.

Proposition (Pigeonhole Principle). Suppose \(f:\mathbb{N}\to\mathbb{N}\) and \(n\ge 0\). If \(f(k)\le n\) for all \(0\le k\le n+1\), then there exist \(0\le k_1,k_2,\le n+1\) such that \(f(k_1)=f(k_2)\).

Formally, this statement is proved by induction on $n$. Further, from a formal proof it is possible to extract an algorithm that, given \(f\) and $n$, will find the required $k_1$ and $k_2$. That is, this algorithm is already implicitly contained in the proof. However, I would guess that for most people, writing such algorithm requires more thought that agreeing that the principle is true. This implies to me that formal proofs often contain details that authors of corresponding paper proofs don't think about.

Now you have complicated matters even more ,because you have added to our arguing a new concept, that of the "formal proof".

If i understand and, correct me if Iam wrong,formal proof isone of the mathematical means that we have at our disposal to examine the correctness of the mathematical proof?

Now before i continue reading carefully your writings i think it would be appropriate to have a definition of the formal proof concept

 

[Evgeny.Makarov]

Now you have complicated matters even more ,because you have added to our arguing a new concept, that of the "formal proof".

My first sentence in post #2 says that mathematical logic provided a precise definition of a mathematical proof. By a formal proof, as opposed to an informal, or plain text, or paper, proof, I mean the concept that was thus defined. A formal proof is a mathematical object that usually takes the form of a sequence or a tree of formulas (which are strings of characters) built according to certain rules.

If i understand and, correct me if Iam wrong,formal proof isone of the mathematical means that we have at our disposal to examine the correctness of the mathematical proof?

Sort of. A formal proof is not a means, but there are means to check whether a given sequence or tree of formulas is a correct formal proof. So, formal proofs make checking possible and even accessible to computers. Perhaps this statement needs qualification, but it is not clear that checking an informal, paper proof is a well-defined problem.

Now before i continue reading carefully your writings i think it would be appropriate to have a definition of the formal proof concept

There are many flavors of formal proofs: natural deduction, sequent calculus, Hilbert system, semantic tableau, lambda calculus and so on. The definitions are somewhat technical. You can find them in Wikipedia. Hilbert system is perhaps the easiest to study, but it is hard to use in practice.

 

[Deveno]

i'm going to be deliberately vague, here. i apologize in advance.

an awful lot depends on what you mean by "correctness".

the best we hope for (in all fairness) is "logical consistency"...that is, the statement we are formulating as a theorem is "by the rules" (there are, unfortunately, competing sets of "rules" available...the one most widely accepted is known as Zermelo-Fraenkel set theory together with a (first or second order) propositional calculus).

some ground-breaking work was done in the 20th century on showing that in many cases, the process of proving something could be reduced to a purely mechanical process (although such a process might be extremely complicated to create). theoretically, one could build an electronic device that when fed a statement in the proper format, would flash a green light if the statement were true, and a red light if the statement were false.

there are, however, problems with "self-reference", once can devise statements which when fed into such a device, would cause it to process indefinitely. that is "provable" statements (in the sense of a formal proof) are a (proper) subset of "true statements". there is some disagreement on whether or not we know what these statements (the true but unproveable ones) actually ARE (the examples used in the various versions of the halting problem, or goedel's incompleteness proof have a certain artificiality to them...these kinds of problems are not the kinds of mathematical statements we are usually most preoccupied with, but serve rather as a test of the limits of our "rule framework").

there is not universal agreement on "what constitutes a proof", although there is some consensus that some statements HAVE been proved (such as 2+2 = 4, with the usual definition of "2", "+", "=" and "4"). in more recent years, the focus has been more on consistency, and "what results go with what assumptions". these differences are more META-mathematical than mathematical...there are differing opinions on "what qualifies as (sound) mathematics" (for example, in the Hilbert system referenced by Mr. Makarov, the axiom:

$(\lnot \phi \rightarrow \lnot \psi) \rightarrow (\psi \rightarrow \phi)$

is not universally accepted, which makes proof by contradiction "suspect" in such a system). in ordinary language, some people don't believe a statement is either true, or false (perhaps there might be an "in-between").

for a certain set of assumptions (namely that classical propositional deductive logic is consistent and sufficient, and that the concept of "set" is well-defined and logically consistent, as specified by the ZF axioms), the consequences have been extensively studied...almost anything you find written in say, a linear algebra textbook (on finite-dimensional vector spaces over countable fields, at least) has been (or in theory COULD be) proven formally in such a mechanical manner. and most (but not all) mathematicians are willing to extend such veracity to say, even infinite-dimensional vector spaces over arbitrary fields (most importantly subfields of the algebraic closure of the metric closure of the rational field, that is to say subfields of the extension $\Bbb C$ of the field $\Bbb R$).

so for your typical theorem (such as the rank-nullity theorem) in a linear algebra text, it is usually deemed sufficient to "build upon the buildings built upon the theorems derived from other theorems that summarize several statements that have been proved from other proved results that were proved directly from the basic axioms". no one, insofar as i know, has been working on an electronic device that will light a green light if and only if the rank and nullity equals the dimension of the domain of an inputted linear transformation in a given vector space. but you COULD.

 

[Evgeny.Makarov]

theoretically, one could build an electronic device that when fed a statement in the proper format, would flash a green light if the statement were true, and a red light if the statement were false.

there are, however, problems with "self-reference", once can devise statements which when fed into such a device, would cause it to process indefinitely. that is "provable" statements (in the sense of a formal proof) are a (proper) subset of "true statements".

There are two separate issues: undecidability in the sense of computation theory and undecidability in the sense of proof theory. The latter sense is used in the title of Gödel's paper ("On Formally Undecidable Propositions in Principia Mathematica and Related Systems"). This sense is outdated, and the term "incompleteness" should be used instead.

Now, even the simplest predicate calculus having in its vocabulary at least one predicate symbol of arity at least 2 is computationally undecidable, so it is not possible to build a machine that says whether a given formula is provable or not. This is true despite the fact that predicate calculus is complete (with respect to all possible models, not w.r.t. one standard model as in the case of arithmetic).

there is some disagreement on whether or not we know what these statements (the true but unproveable ones) actually ARE (the examples used in the various versions of the halting problem, or goedel's incompleteness proof have a certain artificiality to them...these kinds of problems are not the kinds of mathematical statements we are usually most preoccupied with, but serve rather as a test of the limits of our "rule framework").

There are also "natural" examples of statements that are true but not provable in arithmetic, for example, Goodstein's theorem.

 

[solakis1]

There are many flavors of formal proofs: natural deduction, sequent calculus, Hilbert system, semantic tableau, lambda calculus and so on. The definitions are somewhat technical. You can find them in Wikipedia. Hilbert system is perhaps the easiest to study, but it is hard to use in practice.

I did not ask for the flavors of the formal proof , but for the definition of the formal proof.

However in Angelos Margaris book "FIRST ORDER MATHEMATICAL LOGIC",page 13, I found the following definition:

A formal proof is a finite sequence $S_{1}...S_{n}$ of statements such that each $S_{i} (1\leq i\leq n)$ is either an axiom or a definition or a theorem or is inferred from one or more previous $S_{j}'s$ by a rule of inference.The statements $S_{1}...S_{n}$ are called the steps of the proof.

Now according to the set of the rules of inference one uses we have different flavors of formal proofs.

Do you agree to that?

And now to be practical let us consider an easy problem:

In a high school book i found the following proof:

Prove: for all x,y : $|x|<y \Longleftrightarrow -y<x<y$

Proof:

if $x\geq 0$ then we have :

$(|x|<y \wedge x\geq 0)\Longleftrightarrow (x<y \wedge x\geq 0)\Longleftrightarrow 0\leq x<y$...............1

if $x<0$ then we have:

$(|x|<y\wedge x<0)\Longleftrightarrow(-x<y\wedge x<0)\Longrightarrow(x>-y\wedge x<0)\Longrightarrow -y<x<0$.............2

Hence from (1) and (2) we can conclude that the inequality is true only for those x for which $-y<x<y$ holds i.e the following equivalence holds:$|x|<y\Longrightarrow -y<x<y$ for all x,ySince nearly everybody that watches that thread understands that easy proof ,if you apply your procedure of checking the correctness of that proof , then we might come very close in comprehending the procedure you proposed.

 

[Evgeny.Makarov]

However in Angelos Margaris book "FIRST ORDER MATHEMATICAL LOGIC",page 13, I found the following definition:

A formal proof is a finite sequence $S_{1}...S_{n}$ of statements such that each $S_{i} (1\leq i\leq n)$ is either an axiom or a definition or a theorem or is inferred from one or more previous $S_{j}'s$ by a rule of inference.The statements $S_{1}...S_{n}$ are called the steps of the proof.

Now according to the set of the rules of inference one uses we have different flavors of formal proofs.

Do you agree to that?

No, presentations differ not only in axioms, but in the format of derivations, i.e., formal proofs. What you described looks like the Hilbert system, where a derivation is a sequence of formulas. There are other definitions. In one variant of natural deduction a derivation is a tree of formulas. In another variant of natural deduction and in sequent calculus it is a tree of sequents, which are pairs of sets of formulas. Lambda terms is yet another pretty different format, though it is isomorphic to natural deduction.

As I said, Hilbert system is hard to use in practice. Even a derivation of P -> P requires five or six steps.

And now to be practical let us consider an easy problem:

In a high school book i found the following proof:

Prove: for all x,y : $|x|<y \Longleftrightarrow -y<x<y$

Proof:

if $x\geq 0$ then we have :

$(|x|<y \wedge x\geq 0)\Longleftrightarrow (x<y \wedge x\geq 0)\Longleftrightarrow 0\leq x<y$...............1

if $x<0$ then we have:

$(|x|<y\wedge x<0)\Longleftrightarrow(-x<y\wedge x<0)\Longrightarrow(x>-y\wedge x<0)\Longrightarrow -y<x<0$.............2

Hence from (1) and (2) we can conclude that the inequality is true only for those x for which $-y<x<y$ holds i.e the following equivalence holds:$|x|<y\Longrightarrow -y<x<y$ for all x,ySince nearly everybody that watches that thread understands that easy proof ,if you apply your procedure of checking the correctness of that proof , then we might come very close in comprehending the procedure you proposed.

It is possible to manually construct a derivation, say, in natural deduction, but it would not be particularly small, maybe 20 or 30 steps. I could post a lambda term produced by Coq, but without knowing lambda calculus it would make little sense. Note that this proof uses several lemmas, such as ∀x, x < 0 \/ x >= 0 and ∀x, x < 0 -> |x| = -x.

I could also confirm Deveno's words that there is no universal agreement on what constitutes a proof. Thus, in constructive calculus it is not provable that x < 0 \/ x >= 0. It seems restrictive, but the benefit of this system is that proofs of existence of real numbers contain algorithms that allow calculating these numbers to arbitrary precision. But this is a minor quibble for most mathematicians.

 

[solakis1]

No, presentations differ not only in axioms, but in the format of derivations, i.e., formal proofs. What you described looks like the Hilbert system, where a derivation is a sequence of formulas. There are other definitions. In one variant of natural deduction a derivation is a tree of formulas. In another variant of natural deduction and in sequent calculus it is a tree of sequents, which are pairs of sets of formulas. Lambda terms is yet another pretty different format, though it is isomorphic to natural deduction.

As I said, Hilbert system is hard to use in practice. Even a derivation of P -> P requires five or six steps.

It is possible to manually construct a derivation, say, in natural deduction, but it would not be particularly small, maybe 20 or 30 steps. I could post a lambda term produced by Coq, but without knowing lambda calculus it would make little sense. Note that this proof uses several lemmas, such as ∀x, x < 0 \/ x >= 0 and ∀x, x < 0 -> |x| = -x.

I could also confirm Deveno's words that there is no universal agreement on what constitutes a proof. Thus, in constructive calculus it is not provable that x < 0 \/ x >= 0. It seems restrictive, but the benefit of this system is that proofs of existence of real numbers contain algorithms that allow calculating these numbers to arbitrary precision. But this is a minor quibble for most mathematicians.

So we cannot find out whether the above proof is correct or not ??

On the other hand if you think that your process in not so easy for us to understand ,do the procedure on your own and just tell us the verdict.