What is proof to a non-mathematician?

I was talking to Alex this morning and the topic of geometric proof came up. This caused me to spend some time idly thinking about proof. I’ve written about this before but let me expand on it kind of dreamily.

I learned about Coq from a seminar taught by another friend of mine, Tyler Cecil. A key idea I learned from him is audience. The nice and beautiful thing about using a theorem prover like Coq or Lean is that it has the same excruciating standards for everyone. It entices the programmer by making you think that proving something is about the same as writing a program. This is formally true, thanks to the Curry-Howard Isomorphism but the skills needed to write a proof and the skills needed to write a program are curiously different. You wind up needing to know a bit of both to use a theorem prover well.

My friend Randy Van Why explained to me why mathematicians do not especially love theorem provers. In short, they are not solely interested in the truth-value of a proposition. They want to understand why a theorem is true. Input to a theorem prover tells you that a theorem is true, and in many cases it can do a proof-by-exhaustion that human could never pull off. But exhaustively testing every possibility to find out that the four-color theorem is true is not the same as the elegant proof of the five-color theorem. We want to learn something from a proof in addition to the truth value.

Parenthetically, Randy also informed me that the majority of mathematical communication happens over the chalkboard, not paper. So don’t feel bad if you have trouble self-studying math, because mathematicians mostly don’t.

One thing computer scientists like about theorem provers is that they can be restricted to constructive proof. This means certain avenues of proof are unavailable, and some things cannot be proven, but what you can prove, you can also construct—or compute.

However, when I am proving something on the side for fun, the only person I need to convince is myself. Kind of like playing chess with yourself, you have to train yourself a little in how to do it. However, the game is a bit more fun. Often if you don’t know how to do a proof from a book, it’s because you have forgotten an important definition from earlier. Sometimes you misunderstand the situation and make a bad proof you think is good. The time you spend shouting at the page, “this is obvious! why can’t I prove it?” seems to be time well-spent.

Here’s an example from the book No Bullshit Guide to Linear Algebra:

Verify that $|||| = 1$.

Well, we have a few definitions we’ll need to consult:

$|| || = || (v_x,v_y) || =$

and

$=$

Knowing these, we can expand like so:

${\displaystyle \begin{array}{rlr}{\displaystyle \mathrm{\mid }\mathrm{\mid }\widehat{v}\mathrm{\mid }\mathrm{\mid }}& {\displaystyle =}& {\displaystyle \mid \mid \frac{\vec{v}}{\mathrm{\mid }\mathrm{\mid }\vec{v}\mathrm{\mid }\mathrm{\mid }}\mid \mid }\\ {\displaystyle }& {\displaystyle =}& {\displaystyle \mid \mid (\frac{v_x}{\mathrm{\mid }\mathrm{\mid }\vec{v}\mathrm{\mid }\mathrm{\mid }},\frac{v_y}{\mathrm{\mid }\mathrm{\mid }\vec{v}\mathrm{\mid }\mathrm{\mid }})\mid \mid }\\ {\displaystyle }& {\displaystyle =}& {\displaystyle \sqrt{{\left(\frac{v_x}{\mathrm{\mid }\mathrm{\mid }\vec{v}\mathrm{\mid }\mathrm{\mid }}\right)}^2+{\left(\frac{v_y}{\mathrm{\mid }\mathrm{\mid }\vec{v}\mathrm{\mid }\mathrm{\mid }}\right)}^2}}\\ {\displaystyle }& {\displaystyle =}& {\displaystyle \sqrt{{\left(\frac{v_x}{\sqrt{v_x^2+v_y^2}}\right)}^2+{\left(\frac{v_y}{\sqrt{v_x^2+v_y^2}}\right)}^2}}\\ {\displaystyle }& {\displaystyle =}& {\displaystyle \sqrt{\frac{v_x^2}{v_x^2+v_y^2}+\frac{v_y^2}{v_x^2+v_y^2}}}\\ {\displaystyle }& {\displaystyle =}& {\displaystyle \sqrt{\frac{v_x^2+v_y^2}{v_x^2+v_y^2}}}\\ {\displaystyle }& {\displaystyle =}& {\displaystyle \sqrt{1}}\\ {\displaystyle }& {\displaystyle =}& {\displaystyle 1}\end{array}}$

This is a pretty simple example of a direct proof. In my opinion, this is enough detail. Someone newer to this subject matter might be confused by what happened between step 1 and 2, or someone with poor algebra might find the whole thing quite confusing. On the other hand, a more experienced mathematician would probably skip the penultimate step, or maybe even the step before that. The audience matters. But even if it’s just for you, I think doing these kinds of verifications is good for your understanding of the material.

---

---