In mathematics, how do you know when you have proven a theorem?

Two things: You learn that you don’t know, and you learn that deep inside, you do.

When you find, or compose, or are moonstruck by a good proof, there’s a sense of inevitability, of innate truth. You understand that the thing is true, and you understand why, and you see that it can’t be any other way. It’s like falling in love. How do you know that you’ve fallen in love? You just do.

Such proofs may be incomplete, or even downright wrong. It doesn’t matter. They have a true core, and you know it, you see it, and from there it’s only a matter of filling the gaps, cleaning things up, eliminating redundancy, finding shortcuts, rearranging arguments, organizing lemmas, generalizing, generalizing more, realizing that you’ve overgeneralized and backtracking, writing it all neatly in a paper, showing it around, and having someone show you that your brilliant proof is simply wrong.

And this is where you either realize that you’ve completely fooled yourself because you so wanted to be in love, which happens more often when you’re young and inexperienced, or you realize that it’s merely technically wrong and the core is still there, pulsing with beauty. You fix it, and everything is good with the world again.

Experience, discipline, intuition, trust and the passage of time are the things that make the latter more likely than the former. When do you know for sure? You never know for sure. I have papers I wrote in 1995 that I’m still afraid to look at because I don’t know what I’ll find there, and there’s a girl I thought I loved in 7th grade and I don’t know if that was really love or just teenage folly. You never know.

Fortunately, with mathematical proofs, you can have people peer into your soul and tell you if it’s real or not, something that’s harder to arrange with crushes. That’s the only way, of course. The best mathematicians need that process in order to know for sure. Someone mentioned Andrew Wiles; his was one of the most famous instances of public failure, but it’s far from unique. I don’t think any mathematician never had a colleague demolish their wonderful creation.

Breaking proofs into steps (called lemmas) can help immensely, because the truth of the lemmas can be verified independently. If you’re disciplined, you work hard to disprove your lemmas, to find counterexamples, to encourage others to find counterexamples, to critique your own lemmas as though they belonged to someone else. This is the very old and very useful idea of modularization: split up your Scala code, or your engineering project, or your proof, or what have you, into meaningful pieces and wrestle with each one independently. This way, even if your proof is broken, it’s perhaps just one lemma that’s broken, and if the lemma is actually true and it’s just your proof that’s wrong, you can still salvage everything by re-proving the lemma.

Or not. Maybe the lemma is harder than your theorem. Maybe it’s unprovable. Maybe it’s wrong and you’re not seeing it. Harsh mistress she is, math, and this is a long battle. It may takes weeks, or months, or years, and in the end it may not feel at all like having created a masterpiece; it may feel more like a house of sand and fog, with rooms and walls that you only vaguely believe are standing firm. So you send it for publication and await the responses.

Peer reviewers sometimes write: this step is wrong, but I don’t think it’s a big deal, you can fix it. They themselves may not even know how to fix it, but they have the experience and the intuition to know that it’s fine, and fixing it is just work. They ask you politely to do the work, and they may even accept the paper for publication pending the clean up of such details.

There are, sometimes, errors in published papers. It happens. We’re all human. Proofs that are central have been redone so many times that they are more infallible than anything of value, and we can be as certain of them as we are certain of anything. Proofs that are marginal and minor are more likely to be occasionally wrong.

So when do you know for sure? When reviewers reviewed, and time passes, and people redo your work and build on it and expand it, and over time it becomes absolutely clear that the underlying truth is unassailable. Then you know. It doesn’t happen overnight, but eventually you know.

And if you’re good, it just reaffirms what you knew, deep inside, from the very beginning.

Mathematical proofs can be formalized, using various logical frameworks (syntactic languages, axiom systems, inference rules). In that they are different from various other human endeavors.

It’s important to realize, however, that actual working mathematicians almost never write down formal versions of their proofs. Open any paper in any math journal and you’ll invariably find prose, a story told in some human language (usually English, sometimes French or German). There are certainly lots of math symbols and nomenclature, but the arguments are still communicated in English.

In recent decades, tremendous progress has been made on practical formalizations of real proofs. With systems like Coq, HOL, Flyspeck and others, it has become possible to write down a completely formal list of steps for proving a theorem, and have a computer verify those steps and issue a formal certificate that the proof is, indeed, correct.

The motivation for setting up those systems is, at least in part, precisely the desire to remove the human, personal aspects I described and make it unambiguously clear if a proof is correct or not.

One of the key proponents of those systems is Thomas Hales, who developed an immensely complex proof of the Kepler Conjecture and was driven by a strong desire to know whether it’s correct or not. I’m fairly certain he wanted, first and foremost, to know the answer to that question himself. Hales couldn’t tell, by himself, if his own proof is correct.

It is possible that in the coming decades the process will become entirely mechanized, although it won’t happen overnight. As of 2016, the vast majority of proofs are still developed, communicated and verified in a very social, human way, as they were for hundreds of years, with all the hope, faith, imprecision, failure and joy that human endeavors entail.

 

Credit : Quora

Picture Credit : Google