The Social Role of Mathematical Proofs

October 1, 2016

Although proofs are often thought as a way to show beyond reasonable doubt that a mathematical statement is true, this is not always the case in practice, even for mathematicians at the top of the field. Andrew Wiles’s proof of Fermat’s Last Theorem originally contained a gap, and Fields medalist Vladimir Voevodsky found one of his papers to be very wrong seven years after publication.

Mathematical publications are long, and their machinery convoluted. State-of-the-art proofs are by no means a certain way to establish truth, as these proofs are proof-sketchesThe great Dani Wise once said. “Unless you are in the first week of your first-order logic class, all proofs you are going to see are proof-sketches. Deal with it!” . For a long time, I have wondered what the role of a proof is, and where proofs are going with the advancement of computing power and formal verification.

Recently, I had the occasion to attend a seminar at Tufts given by Kenny Easwaran which addresses these very questions. Here’s my takeaway.

Using today’s computing power, there are three main ways that mathematical proofs can be going:

Probabilistic results (experimental math)

Let’s use a toy argument to illustrate the premise of experimental math.

Suppose I want to prove that some $p$ is a very large prime. Fermat’s Little Theorem says that for all $a < p$, $a^{p-1}$ is congruent to $1 \mod p$. Note that $a^{p-1} = 1 \mod p$ for all $a < p$ does not imply that $p$ is necessarily primeNumbers $p$ which are not prime but still satisfy the congruence relation for all $a$ relatively prime to $p$ are known as Carmichael numbers. , but for very large $p$, and large sample of $a$’s, we may compute a probability of $p$ being prime. Suppose we narrow the probability of being wrong to the order of $10^{-20}$ using computational techniques. Then, this probability of $p$ being prime using our experimental technique is much higher than the probability of a published mathematical proof using today’s standards being right, in which case we are done.

If the role of proofs is to develop confidence A higher probability of something being true. that a mathematical statement is true, this probabilistic result by all means gives a better confidence than most published proofs, assuming we trust the authors of the experiments have picked a truly “random”, or representative sample. (This is also known as transferability The concept of not having to trust the author to trust the result. In experimental math just like in other experimental fields, results are not generally transferable because we have to trust that the authors truly conducted the experiment the way they described it. For example, if the authors say that they picked a random sample, we have to trust that the sample they picked is truly random. .)

But to most mathematicians, this experimental math framework just feels wrong. That’s because we like certainty, or the possibility of it. Which brings us to:

Formal Verification

If the role of proofs is to establish certainty, then we can write out proofs from essentially first-order logic and have a computer check it. Due to their format, formal verification proofs as of now are hard for a human to read and understand. Here’s an exampleCredit: Mike Nahas. of the basic proof that equality is transitive, i.e. that $x = y, y = z \Rightarrow x = z$ in Coq:

Proof.
  intros x y z.
  intros x_y y_z.
  destruct x_y as [].
  destruct y_z as [].
  exact (eq_refl x).
Qed.

In practice, these formal verification proofs do not give us certainty for the truth of a mathematical statement via our personal understanding, but via the understanding of the proof by an idealized rational reader, the computer. If the goal of mathematics is to communicate human understandingSee the beautiful essay On Proof and Progress in Mathematics by William Thurston. , then formal verification doesn’t quite do it.

Traditional proofs

Compared to the two methods above, proofs in the usual sense are less certain and not as good at establishing confidence than experimental math methods. However, they do a decent job at communicating.

Indeed, they are transferable to an extent because someone who reads a proof is reconstructing the results in their heads and checking them (this is not typically done if someone is reading an experimental result I believe this problem could be solved for mathematical experiments, which is mostly generating data using an algorithm, by providing the algorithm in clean code along with the publication, which would allow the readers to verify the data for themselves. ).

Proofs also gives us a good structure to think about mathematical facts, known as convertibility If there exists a counterexample of a proof, we can generally figure out in which way our proof is wrong. . Let’s establish the following analogy: if an environmentalist tells you climate change is real, and gives you overview the temperature changes of the past 10,000 years, you are likely to believe her. Now, if she later tells you that there has been a major error in measuring carbon levels of the 1800s, you are unlikely to know how to update your mental model of climate, unless you are a climate scientist.

In contrast, if you read Cauchy’s proof that every sequence of continuous functions converges to a continuous function Sørosen, H. (2005). Understanding Abel’s comment on Cauchy’s theorem. Historia Mathematica, 32:453-490. :

Let $s_n$ be the sequence of continuous functions, and let $s$ be the function that is its limit. Because $s_n \to s$, we have $s(x+\alpha) - s_n(x+\alpha) \to 0$ as $n \to \infty$, and $s_n(x) - s(x) \to 0$ as $n \to \infty$. Because each $s_n$ is continuous, we have $s_n(x + a) - s_n(x) \to 0$ as $\alpha \to 0$. Putting this all together, we have $s(x+\alpha) - s(x) = [s(x+\alpha) - s_n(x + \alpha)] + [s_n(x+\alpha)-s_n(x)] + [s_n(x) - s(x)]$, and $\alpha \to 0$ and $n \to \infty$, this sum must go to $0$. Thus, $s$ is continuous at $x$.

and take the counterexample of the Fourier series $\sum_{i=1}^\infty (-1)^{n+1}\frac{\sin nx}{n}$ of the sawtooth function (illustrated below):

you can get a sense that Cauchy’s proof is wrong because Cauchy is assuming uniform convergence, not (pointwise) convergence of the functions. In particular, the implicit quantifiers $\forall$ (for all) and $\exists$ (there exists) are presented in the wrong order Recall that pointwise convergence for a sequence of functions ${f_n}$ to $f$ is defined as $\forall x, \forall \varepsilon$, $\exists N(\varepsilon, x)$ such that for $n \geq N(\varepsilon,x)$, $|f_n(x) - f(x)| < \varepsilon$ whereas uniform convergence is defined as $\forall \varepsilon, \exists N(\epsilon)$ such that $\forall x, n \geq N(\epsilon)$ implies $|f_n(x- f(x)| < \epsilon$. , which is an easy mistake to make because the order of quantifiers isn’t clear from conversational language.

Conclusion

Easwaran’s seminar was a great discussion, and helped me have a clearer idea of what is meant by mathematical progress. I feel lucky to have attended such a seminar so early in my career (thanks to Moon Duchin), and I look forward to applying all three forms of mathematical progress in my own research.

The Social Role of Mathematical Proofs

Probabilistic results (experimental math)

Formal Verification

Traditional proofs

Conclusion

Further Readings