<p>Software engineers have a notion they call "<a href="http://en.wikipedia.org/wiki/Code_smell"><strong>code smells</strong></a>".  These are symptoms in the code that may indicate a deeper problem.  Software engineers collect mental lists of smells to be aware of (i.e. excessively long methods or too many parameters).  It does not necessarily mean there is a problem, but simply indicate that the writer might want to double check.</p>

<p>I propose that we ought to also consider <strong>"proof smells"</strong>.  This will not give you an algorithm for checking your proofs but it gives a language and a metaphor for recognizing possible problems in proofs.  Some examples of proofs smells:</p>

<ol>
<li>The adverbs "Clearly", "Obviously", etc.</li>
<li>Reference to the proof of a previous result instead of a reference to the result itself.</li>
<li>Flippant use of a result with many technical preconditions.</li>
</ol>

<p>There are also more subtle smells.  For example, if a proof uses the binomial theorem to expand an expression and then later uses the binomial theorem to return to a closed form, then maybe there is a direct manipulation on the closed form that gives the same result. </p>

<p>My suggestion is to collect a (mental or written) list of such smells and check for them as you read through your work.  The nice side effect of this approach is that it will also make you a better reader.</p>

<p><em>Note: My hope in this answer was to give intuitive side to the rigorous answer supplied by Lamport's How to Write a Proof referenced in M. Alaggan's answer.</em></p>

CC BY-SA 3.0
2011-05-16T16:13:14.737Z
I say this all the time to my students, and they think I'm crazy. Of course I actually claim I can smell a bug, which might be part of the problem ;)
Suresh Venkat
CC BY-SA 3.0
2011-05-16T20:16:18.773Z
@Suresh: This student thinks you're crazy for different reasons. ;-)
Josephine Moeller
CC BY-SA 3.0
2011-05-16T20:20:21.640Z
On the code smell note, things I always try to scrutinize in others' proofs include inequality chains. Often really basic errors have a habit of creeping in amongst the more difficult derivations.
Josephine Moeller
CC BY-SA 3.0
2011-05-16T15:43:36.023Z
2011-11-02T16:37:17.637Z
2011-11-02T16:37:17.637Z
Don Sheehy
<p>There is a very good paper by Leslie Lamport (<a href="http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-how-to-write" rel="nofollow noreferrer">How to write a proof</a>). It is actually a proposal by him on a style of writing detailed proofs in such a way that:</p>

<p>(1) Allows detecting errors in a straight-forward way </p>

<p>(2) Makes it clear which assumptions and theorems used in which parts, which makes it pretty easy to see what happens if you want to (for instance) use weaker assumptions</p>

<p>There is also some <a href="https://mathoverflow.net/questions/35727/community-experiences-writing-lamports-structured-proofs">community experience</a> and inspiring commentary on this technique on MO which shows positive experience in general (and some other resources as well). </p>

<p>Update: there is a new version <a href="http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf" rel="nofollow noreferrer">How to write a 21st century proof</a>.</p>

CC BY-SA 3.0
2011-05-16T05:33:35.460Z
These proofs are very similar to what one would write in a PL research paper. The chain of logic is very explicit. After learning how to read and appreciate PL-style proofs, I've found it difficult to make sense of "normal" math proofs. Such proofs  often require that the reader think in the same way the author does, and when you've gotten used to a different proof style, this is simply not the case (for me, at least!)
Christopher Monsanto
CC BY-SA 3.0
2011-05-16T09:34:36.730Z
@Christopher Monsanto: PL stands for Programming Languages ? I would appreciate if you can mention such an example (one such paper) to check out :)
Mohammad Alaggan
CC BY-SA 3.0
2011-05-16T13:24:05.163Z
I always had the feeling that what Lamport suggest is not compatible with Paul Lockhart's "A Mathematician's Lament" (http://www.maa.org/devlin/LockhartsLament.pdf).
Marcos Villagra
CC BY-SA 3.0
2011-05-16T04:18:46.163Z
2016-03-15T09:38:30.700Z
2017-04-13T12:57:54.777Z
Mohammad Alaggan
<p>I seem to remember reading a popular account long ago of how physicists deal with an analogous problem. Who knows how accurate the following version of it is; corrections are welcome. But I found the underlying strategy quite remarkable.</p>

<p>They explained how they came to believe in black holes. Black holes were initially purely mathematical constructs, like other strange objects in physics like wormholes. Their strategy was striking: they would mathematically throw other objects at the object to be tested. Wormholes failed their tests because they found that the wormhole would collapse even in the presence of a normal physical object, maybe an asteroid. But black holes passed this test: the black hole would survive having an asteroid thrown at it. So they tried throwing a star at it. Same result. Finally, they threw another black hole at the black hole and it survived. As a result of this, they grew confident enough in the existence of black holes to actually start looking for them in the real universe.</p>

<p>So the relevance and application of the strategy above is to start throwing things at your proof. Does it survive <a href="http://www.scottaaronson.com/blog/?p=458">sanity checks</a>? If you remove a necessary assumption, does it collapse as it should? Does it collapse as it should when it's applied to cases outside its scope? Does it withstand reasonable generalizations and specializations? Have a look at the <a href="http://en.wikipedia.org/wiki/How_to_Solve_It#Heuristics">list of heuristics</a> in Polya's <i>How to Solve It</i>. Try mutating your proof with these heuristics and see if it stands and falls as it should. </p>

CC BY-SA 3.0
2014-02-19T09:24:16.863Z
Most of your answer focuses on checking proofs by verifying that they become false in situations where they should be false. That doesn't work because it doesn't check that the theorem was true where it was supposed to be true! For example, suppose that I've "proved" that every odd number is divisible by three. I check that my proof fails if I extend to even numbers too: it does, since four is not divisible by three. Hooray, my proof must be correct!
David Richerby
CC BY-SA 3.0
2011-05-17T22:10:04.807Z
2011-05-17T22:10:04.807Z
ShyPerson
<p>I think one of the safest approaches is to come up with multiple independent proofs. Then you can be confident that your main result is correct, even if you have a mistake in some details of a proof.</p>

CC BY-SA 3.0
2011-05-16T09:06:05.377Z
2011-05-16T09:06:05.377Z
Jukka Suomela
<p>Dick Lipton has a nice article titled '<a href="http://rjlipton.wordpress.com/2010/07/11/proving-a-proof-is-a-proof/">How to Prove a proof is a proof</a>'</p>

CC BY-SA 3.0
2011-05-16T16:18:32.483Z
2011-05-16T16:18:32.483Z
Suresh Venkat
<p>One technique I've found useful is to think about what other results would the proof strategy be able to prove. If I'm easily able to adapt the proof strategy to prove a big open problem or even a problem that isn't open but which has a much too complicated solution compared to the complexity of the proof strategy, then that's a big reason to doubt the proof.</p>

CC BY-SA 3.0
2014-02-19T02:34:17.827Z
I'd give this +10 if I could - particularly in complexity theory, flawed proof techniques can often be shown to prove really strong statements like $P \neq NP$, and then it's very easy to guess that your proof technique is wrong. Particularly if your proof technique relativizes!
Joshua Grochow
CC BY-SA 3.0
2011-11-03T11:58:58.030Z
2011-11-03T11:58:58.030Z
Opt
<p>I always re-check my proofs with a proof-checker like <a href="http://en.wikipedia.org/wiki/Coq" rel="nofollow">COQ</a> or <a href="http://en.wikipedia.org/wiki/Isabelle_%28proof_assistant%29" rel="nofollow">ISABELLE</a>. If you can prove your proof in any of these programming language, you can be sure your proof is correct. As simple as a lambda-term ;).</p>

CC BY-SA 3.0
2011-05-17T00:17:08.853Z
I've never used Coq, but I ought to try. In fact, I'm trying to prove some lower bounds with mathematica, but I haven't found the right way. Maybe I need some special packages or something.
Marcos Villagra
CC BY-SA 3.0
2011-05-17T13:57:03.360Z
Maybe it a longshot, but if you want to prove some lower bounds with reals, you can check these libraries: http://coqtail.sourceforge.net/?home/en
Gopi
CC BY-SA 3.0
2014-02-19T17:00:51.797Z
Agreed, but any programming language works. Most often I do this in reverse. Formulate the problem domain in a programming language (usually Ruby), then use this as a template for my proof.
Chad Brewbaker
CC BY-SA 3.0
2011-05-16T15:59:20.227Z
2014-02-19T10:01:43.570Z
2014-02-19T10:01:43.570Z
Gopi
<p>What are general guidelines for checking your proofs? I believe this is important for graduate students like me. I already know what we need to do to prove something, but you always have to check everything before you send it out. Even to your own advisor.</p>

<p>I've developed myself some strategies by trial and error, and got a lot of advice from my advisor. But this is always a very tedious work. Normally, when you finish with something, you just want to go on to the next problem, but you still have to stick to the current problem until everything is perfect. Here I present an example of my own list of tricks:</p>

<ol>
<li>Fill in the details. A lot of mistakes are in places were you write "it is clear that...", "without loss of generality...", etc.</li>
<li>Try some numbers. Try extreme cases, like "what happens when I set $n=1$ or $n=1000$".</li>
<li>Keep a clean notebook. Write every day on it, and compare it with your rough notes. I try to write also in latex, I've found many mistakes this way.</li>
</ol>

<p>What are the general strategies that you apply for checking your proofs?</p>

<p>The objective of this question is to make it a community-wiki.</p>

CC BY-SA 3.0
2011-05-16T01:56:10.387Z
If the question appears subjective, please help me improve it.
Marcos Villagra
CC BY-SA 3.0
2011-05-16T02:24:14.013Z
how do I make this community-wiki?
Marcos Villagra
CC BY-SA 3.0
2011-05-16T02:35:35.903Z
Hey, cool! I'm really interested in the answers to this question.

Also, I can appreciate your #3. (When I think about it, I actually have piles of paper scattered everywhere when I'm intently working on a problem, which then get randomly relocated. Yuck.) I've run into an mistake before from this very issue and ended up wasting a good chunk of time.
Daniel Apon
CC BY-SA 3.0
2011-05-16T02:45:05.000Z
@Daniel: I had the same problem!! That's why after I finnish with a proof, I immediately write the latex version. Its good to know that I'm not the only messy guy that keeps everything everywhere :-)
Marcos Villagra
CC BY-SA 3.0
2011-05-16T16:11:54.020Z
you flag it for moderator attention.
Suresh Venkat
<soft-question><research-practice><writing>
How to shoot down your proofs
Marcos Villagra
# How to shoot down your proofs

(Asked by: username_0 on 2011-05-16)

What are general guidelines for checking your proofs? I believe this is important for graduate students like me. I already know what we need to do to prove something, but you always have to check everything before you send it out. Even to your own advisor.

I've developed myself some strategies by trial and error, and got a lot of advice from my advisor. But this is always a very tedious work. Normally, when you finish with something, you just want to go on to the next problem, but you still have to stick to the current problem until everything is perfect. Here I present an example of my own list of tricks:

1. Fill in the details. A lot of mistakes are in places were you write "it is clear that...", "without loss of generality...", etc.
2. Try some numbers. Try extreme cases, like "what happens when I set $n=1$ or $n=1000$".
3. Keep a clean notebook. Write every day on it, and compare it with your rough notes. I try to write also in latex, I've found many mistakes this way.

What are the general strategies that you apply for checking your proofs?

The objective of this question is to make it a community-wiki.

**Tags:** soft-question, research-practice, writing
> **Comments:**
> **username_0**: If the question appears subjective, please help me improve it.  
> **username_0**: how do I make this community-wiki?  
> **username_1**: Hey, cool! I'm really interested in the answers to this question.  Also, I can appreciate your #3. (When I think about it, I actually have piles of paper scattered everywhere when I'm intently working on a problem, which then get randomly relocated. Yuck.) I've run into an mistake before from this very issue and ended up wasting a good chunk of time.  
> **username_0**: @Daniel: I had the same problem!! That's why after I finnish with a proof, I immediately write the latex version. Its good to know that I'm not the only messy guy that keeps everything everywhere :-)  
> **username_2**: you flag it for moderator attention.  

---

## 7 answers

### Answer by username_3 on 2011-05-16. Score: 42

Software engineers have a notion they call "[**code smells**](http://en.wikipedia.org/wiki/Code_smell)". These are symptoms in the code that may indicate a deeper problem. Software engineers collect mental lists of smells to be aware of (i.e. excessively long methods or too many parameters). It does not necessarily mean there is a problem, but simply indicate that the writer might want to double check.

I propose that we ought to also consider **"proof smells"**. This will not give you an algorithm for checking your proofs but it gives a language and a metaphor for recognizing possible problems in proofs. Some examples of proofs smells:

1. The adverbs "Clearly", "Obviously", etc.
2. Reference to the proof of a previous result instead of a reference to the result itself.
3. Flippant use of a result with many technical preconditions.

There are also more subtle smells. For example, if a proof uses the binomial theorem to expand an expression and then later uses the binomial theorem to return to a closed form, then maybe there is a direct manipulation on the closed form that gives the same result.

My suggestion is to collect a (mental or written) list of such smells and check for them as you read through your work. The nice side effect of this approach is that it will also make you a better reader.

*Note: My hope in this answer was to give intuitive side to the rigorous answer supplied by Lamport's How to Write a Proof referenced in M. Alaggan's answer.*

> **Comments:**
> **username_2**: I say this all the time to my students, and they think I'm crazy. Of course I actually claim I can smell a bug, which might be part of the problem ;)  
> **username_4**: @Suresh: This student thinks you're crazy for different reasons. ;-)  
> **username_4**: On the code smell note, things I always try to scrutinize in others' proofs include inequality chains. Often really basic errors have a habit of creeping in amongst the more difficult derivations.  

---

### Answer by username_5 on 2011-05-16. Score: 24

There is a very good paper by Leslie Lamport ([How to write a proof](http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-how-to-write)). It is actually a proposal by him on a style of writing detailed proofs in such a way that:

(1) Allows detecting errors in a straight-forward way

(2) Makes it clear which assumptions and theorems used in which parts, which makes it pretty easy to see what happens if you want to (for instance) use weaker assumptions

There is also some [community experience](https://mathoverflow.net/questions/35727/community-experiences-writing-lamports-structured-proofs) and inspiring commentary on this technique on MO which shows positive experience in general (and some other resources as well).

Update: there is a new version [How to write a 21st century proof](http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf).

> **Comments:**
> **username_6**: These proofs are very similar to what one would write in a PL research paper. The chain of logic is very explicit. After learning how to read and appreciate PL-style proofs, I've found it difficult to make sense of "normal" math proofs. Such proofs  often require that the reader think in the same way the author does, and when you've gotten used to a different proof style, this is simply not the case (for me, at least!)  
> **username_5**: @Christopher Monsanto: PL stands for Programming Languages ? I would appreciate if you can mention such an example (one such paper) to check out :)  
> **username_0**: I always had the feeling that what Lamport suggest is not compatible with Paul Lockhart's "A Mathematician's Lament" (http://www.maa.org/devlin/LockhartsLament.pdf).  

---

### Answer by username_2 on 2011-05-16. Score: 15

Dick Lipton has a nice article titled '[How to Prove a proof is a proof](http://rjlipton.wordpress.com/2010/07/11/proving-a-proof-is-a-proof/)'


---

### Answer by username_7 on 2011-05-17. Score: 14

I seem to remember reading a popular account long ago of how physicists deal with an analogous problem. Who knows how accurate the following version of it is; corrections are welcome. But I found the underlying strategy quite remarkable.

They explained how they came to believe in black holes. Black holes were initially purely mathematical constructs, like other strange objects in physics like wormholes. Their strategy was striking: they would mathematically throw other objects at the object to be tested. Wormholes failed their tests because they found that the wormhole would collapse even in the presence of a normal physical object, maybe an asteroid. But black holes passed this test: the black hole would survive having an asteroid thrown at it. So they tried throwing a star at it. Same result. Finally, they threw another black hole at the black hole and it survived. As a result of this, they grew confident enough in the existence of black holes to actually start looking for them in the real universe.

So the relevance and application of the strategy above is to start throwing things at your proof. Does it survive [sanity checks](http://www.scottaaronson.com/blog/?p=458)? If you remove a necessary assumption, does it collapse as it should? Does it collapse as it should when it's applied to cases outside its scope? Does it withstand reasonable generalizations and specializations? Have a look at the [list of heuristics](http://en.wikipedia.org/wiki/How_to_Solve_It#Heuristics) in Polya's *How to Solve It*. Try mutating your proof with these heuristics and see if it stands and falls as it should.

> **Comments:**
> **username_8**: Most of your answer focuses on checking proofs by verifying that they become false in situations where they should be false. That doesn't work because it doesn't check that the theorem was true where it was supposed to be true! For example, suppose that I've "proved" that every odd number is divisible by three. I check that my proof fails if I extend to even numbers too: it does, since four is not divisible by three. Hooray, my proof must be correct!  

---

### Answer by username_9 on 2011-05-16. Score: 11

I think one of the safest approaches is to come up with multiple independent proofs. Then you can be confident that your main result is correct, even if you have a mistake in some details of a proof.


---

### Answer by username_10 on 2011-11-03. Score: 8

One technique I've found useful is to think about what other results would the proof strategy be able to prove. If I'm easily able to adapt the proof strategy to prove a big open problem or even a problem that isn't open but which has a much too complicated solution compared to the complexity of the proof strategy, then that's a big reason to doubt the proof.

> **Comments:**
> **username_11**: I'd give this +10 if I could - particularly in complexity theory, flawed proof techniques can often be shown to prove really strong statements like $P \neq NP$, and then it's very easy to guess that your proof technique is wrong. Particularly if your proof technique relativizes!  

---

### Answer by username_12 on 2011-05-16. Score: 6

I always re-check my proofs with a proof-checker like [COQ](http://en.wikipedia.org/wiki/Coq) or [ISABELLE](http://en.wikipedia.org/wiki/Isabelle_%28proof_assistant%29). If you can prove your proof in any of these programming language, you can be sure your proof is correct. As simple as a lambda-term ;).

> **Comments:**
> **username_0**: I've never used Coq, but I ought to try. In fact, I'm trying to prove some lower bounds with mathematica, but I haven't found the right way. Maybe I need some special packages or something.  
> **username_12**: Maybe it a longshot, but if you want to prove some lower bounds with reals, you can check these libraries: http://coqtail.sourceforge.net/?home/en  
> **username_13**: Agreed, but any programming language works. Most often I do this in reverse. Formulate the problem domain in a programming language (usually Ruby), then use this as a template for my proof.  

---

