Yes: At the Very Least, Trivial Proofs
If you’re very verbose, you can write down your axiom schema, perhaps starting with David Hilbert’s six rules of logic or the axioms of Natural Deduction, the axioms of equality, set theory or Peano arithmetic, and so on. Many mathematicians use automated proof checking to verify the correctness of a proof, or even proof-assistant software. If the one mathematician on Earth is also a competent programmer, he or she will be able to write a simple program to parse a formal proof and verify its validity through pure symbol manipulation. When you specify which theorem or axiom justifies each transformation of the well-formed formula on each line of the proof, there’s no ambiguity about what it means for the proof to be correct or incorrect given its premises and axioms.
But Only the Most Trivial Proofs Are Like That
I posted a simple little proof to Math.SX a few days ago. It tries to be simple and elementary, spelling out the steps that the other answers and comments left the reader to work out for themselves. The first comment it got was, “The best answer for us folks who aren’t so math savvy.”
There are a lot of gaps in it, and it assumes that the audience is comfortable with high-school algebra. I suspect that a lot of people who aren’t regular readers of a math website would have the same reaction to seeing me go from ln u + ln v - ln u to ln (u·v/u) that I do to skimming a short proof from a branch of mathematics I haven’t used in twenty years. I don’t bother to explain why that’s valid. Nor do I explain why you add constants of integration when taking the indefinite integral of both sides of an equation, or why you can move the two constants to a single constant on one side.
I could. If I’d spelled out every step of the transformation from ln u + C₁ = ln v + C₂ to ln u = ln v + C, it might have gone something like this:
We’re implicitly, although the question didn’t specify one, working in a mathematical structure called a field. Since we defined u and v as functions of some variable x and need the natural logarithm to be a valid operation for all values of u and v, Given the context, it’s likely that x is a positive real number, and u and v are positive. Neither the original question nor my proof ever spelled this out, and other interpretations are possible, but that’s what a mathematician writing in English in the early twenty-first century would assume the question meant by default. So I stay somewhat agnostic: I implicitly assume that the range of ln u and ln v is some field, but not which, and I don’t spell that assumption out.
That allows me to add, subtract, multiply, divide, and take additive and multiplicative inverses. In particular, it lets me construct the constant -C₁ such that C₁ + (-C₁) = 0.
A formal, step-by-step, proof from this point on where every step is justified by exactly one standard axiom might look like this:
- ln u + C₁ = ln v + C₂ (By Previous Lemma)
- ln u + C₁ + (-C₁) = ln v + C₂ + (-C₁) (Additive property of equality)
- ln u + [C₁ + (-C₁)] = ln v + C₂ + (-C₁) (Associativity of addition)
- ln u + 0 = ln v + C₂ + (-C₁) (Definition of additive inverse)
- ln u = ln v + C₂ + (-C₁) (Definition of additive identity)
- ln u = ln v + [C₂ + (-C₁)] (Associativity of addition)
- Let C = C₂ + (-C₁) (Definition)
- ln u = ln v + C (Substitution property of equality)
Even after that handwaving ahead of time about how I’m assuming all the terms here are elements of some field, there’s still some hand-waving left. I said that C is a constant, but to actually prove that, I might show that it’s the difference of two constants, a special case of applying a pure function to constant inputs. And of course I use a lot of shorthand and take for granted a lot of mathematics that not every mathematician in history would have accepted, for example, that ln u and ln v are well-defined.
I didn’t write out the steps in that level of detail, because I was writing for humans (who would have found it tedious and patronizing), not a computer. A proof written to be as easy as possible for a computer to parse algorithmically would have looked very different. But, even if I were writing a proof checker for my own use, as the last mathematician on Earth, I’d find it a lot more interesting to figure out how to make it smart enough to fill in more of those gaps itself than I would to write every proof that way.
Nobody ever does that. It would take forever, waste a lot of space, and annoy everybody.
What about Srinivasa Ramanujan?
He’s the most famous example of an autodidact who wrote down amazing results in notebooks, which other mathematicians don’t consider “proofs.” This is probably because he worked out the derivations and notes on a piece of slate, wrote down what he considered the important results, and then erased the slate to save money. He wasn’t really trying to “prove” anything to some mathematician in Britain yet.
If the only mathematician in the world learned that way, his personal writings would probably be like that: not really intended to convince anyone else. (One philosopher’s comment on the earliest known proof in Greece, that the area of both halves of a circle split by a line through its center is the same, is that the real brilliance of it was not the argument, but realizing that a proof was needed.) Are his notebooks “proofs?” The fewer steps he skips—or the more that the steps he skips fit into a pattern of regular examples that a reader could figure out to reconstruct his thought process—the more proof-like they are.
I think the important question is, what happens if the world’s only mathematician takes on a student? Even someone who finds his lost notebook years after he died (which also happened to Ramanujan). If the student thinks his writings constitute a convincing argument that the teacher hasn’t made a mistake somewhere, even when they results are counterintuitive, and they don’t need to be taken on faith, it’s probably a sort of “proof.”