Non-rigorous reasoning in rigorous mathematics I was wondering what role non-rigorous, heuristic type arguments play in rigorous math. Are there examples of rigorous, formal proofs in which a non-rigorous reasoning still plays a central part?
Here is an example of what I am thinking of. You want to prove that some formula $f(n)$ holds, and you want to prove this by induction. Based on heuristic arguments, you conjecture what the correct formula is. Then you prove it by induction. But, if you had just given the induction proof on its own, then you would have to pluck this mysterious formula out of thin air.
I am interested in situations in which there is a heuristic argument which is valid and can be formalized. I am more interested in cases in which there is a heuristic argument and a separate (or complementary) rigorous argument, but the heuristic argument is more enlightening and more explanatory.
 A: The genus–degree formula says that genus $g$ of a nonsingular projective plane curve of degree $d$ is given by the formula $g = (d-1)(d-2)/2$.  Here is a heuristic argument for the formula. Take $d$ lines in general position in the plane; collectively these form a (singular) degree-$d$ curve.  There are $d \choose 2$ points of intersection.  Now think in terms of complex numbers and visualize each line as a Riemannian sphere.  If you start with $d$ disjoint spheres and then bring them together so that every one touches every other one (deforming when necessary) then you expect the genus of the resulting surface to be ${d \choose 2} - (d-1) = (d-1)(d-2)/2$, because after you connect them together in a line with $d-1$ connections, each subsequent connection increases the genus by one.
I find this argument to be, at minimum, a good way to remember the formula, and I seem to recall reading that there does exist a rigorous proof along these lines, but I've never actually seen one.
More generally, there are lots of examples of the sort of thing you're looking for in enumerative algebraic geometry.  Hilbert's fifteenth problem asked for a rigorous foundation for the Schubert calculus; today we would regard Schubert's methods as heuristic, although I believe that all his calculations have now have proofs that are rigorous by modern standards.  String theory has also predicted enumerative formulae by what mathematicians would consider heuristic means; in one famous example, the physicists Candelas et al. predicted a formula that the mathematicians Ellingsrud and Strømme at first thought they could disprove, but later the mathematicians found a mistake in their argument and the physicists were vindicated.
A: You do "pluck the mysterious formula from thin air". That is why there are (not enough) jobs available to mathematicians: Doing Math is not something you can leave to a computer program. 
The german word ansatz describes this mental process very well. To solve a system of linear ODEs you assume the solutions are exponentials, and then proceed to find the coefficients. This assumption step is where intuition takes place.
Of course this example is old, trivial, and well known, but similar insights are part of all new results. Your intuition shows you the way and THEN you formalize the proof.
A: In mathematical statistics people often have experience about some method that works well in practice even though it "shouldn't" in all generality.  The game is then to ask what conditions need to be satisfied to explain why the method works.  
Here is an example which I was not personally involved in, so I can only speculate.  This paper by Bickel and Li considers local polynomial regression methods and shows that they works as well as possible (in the sense of asymptotic optimality) when the data it is being used on has low dimensional structure. The idea is that people were finding that certain regression techniques were giving reasonable generalization performance in prediction problems even when the data was high dimensional so they figured that maybe the data wasn't actually high dimensional in some relevant aspect.  But which relevant aspect, that's the challenging part.
To my mind, figuring out how to explicitly articulate the minimal conditions under which some ``obvious" fact is true is where the discover and understanding come in.   It is a very different process than what a student does on problem set, where the statement and all the relevant conditions are laid out and the main job is deriving the stated implication.
Put another way: research has degrees of freedom on both ends -- you can find/create the answer and the question as pairs, rather than being handed the one and being asked to complete the set.  This perspective of course doesn't cover all cases -- notably, that of people chasing down famous open problems. But it is a way in which one can develop a rigorous understanding from ``non"-rigorous reasoning.  When one first starts thinking vaguely about a problem there is nothing there about which to be rigorous.
A: In 1965 I had the idea that the proof of the Seifert-van Kampen theorem for the fundamental groupoid generalised to two dimensions, and higher, but lacked the gadget corresponding  a 2-dimensional fudamental groupoid using squares composed in two directions. So this was an idea of a proof in search  of a theorem.  So I tried  for 9 years to define this for a topological space. Finally, in 1974, Philip Higgins and I realised that we could do this for a pair of spaces, i.e. a space $X$ and subspace $A$, mapping a square to $X$ with edges mapped into $A$ and taking homotopy classes of these maps with vertices fixed in the homotopies. Fortunately, lots of work on related algebra had been done in the meanwhile, so the main stuff rolled out, and got published in 1978. 
Unfortunately, the use of groupoids and double groupoids seemed to arouse hostility. so this and the work in all dimensions was, a colleaue remarked, pursued in the teeth of opposition! 
So that is another possible affect of intuition. to say some work is ridiculous! It's a hard life! But has been lots of fun pursuing a line of intuition and trying to make it really work. I was lucky in my collaborators, too. 
Later: There is an example in J.E. Littlewood's "A mathematican's miscellany" where a picture contains the essential argument. In higher category theory, there is quite a lot of use of manipulating diagrams, and this is regarded, rightly,  as rigorous. 
A: Every geometric problem that has a two-dimensional representation
is solved by almost every mathematician by first drawing a diagram, then deriving the correct formal description from this diagram, and then continuing to solve the problem in
the algebraic description.
These certainly are ubiquitous "situations in which there is a heuristic argument which is valid and can be formalized."
Also the heuristic argument is "separate (or complementary)" to the  "rigorous argument, but the heuristic argument is more enlightening and more explanatory."
A: To me, the quintessential example of the employment of non-rigorous reasoning to arrive at rigorous proofs is Archimedes' On method, where he employs a "mechanical" method, usually called the method of indivisibles, as a heuristic, to arrive at results which he then proves with the method of exhaustion. Even better, Archimedes acknowledges and explains this way of proceeding in the work itself, where he draws the distinction between discovering new results on the one hand (θεωρεῖν), and the subsequent rigorous proving of the results (ἀποδεικνύναι). 
Somehow, this feels remarkably similar to Grothendieck's description of his theory of motives as an instrument of discovery.
A: In elementary calculus, the way I was taught to integrate by partial fractions was to guess the numerators of the fractions, then back-substitute to check the correctness of the guess.  Very often the guess would be right for no obvious reason.  When it was wrong, the discrepancy immediately suggested (non-rigorously) what the next guess should be, and the second guess was almost always correct.
A: Let me expand on the example of infinitesimal calculus, with
its $dx$ as infinitesimal increment. All the non rigorous computations 
made by mathematicians and physicists were finally formalized
in the encyclopedie de Diderot by D'Alembert 
who introduced the $\varepsilon-\delta$ definition of limit and continuity.
Yet physicists still stick to the "infinitesimal displacement"
heuristics in their courses and I think that this viewpoint
is a key part of our understanding of calculus.
The same story repeats with harmonic analysis and the 
non-rigorous computations of Fourier, the symbolic calculus
of Heavyside, finally put on firm grounds by L. Schwartz 
with the theory of distributions. Notations such as
$\int_{\bf R} e^{itx} dx = 2\pi \delta_0(t)$ are still very much
in flavor in physics courses and lead to elegant proofs 
of the standard formulas of harmonic analysis such as 
Fourier inversion. And then of course there are the Feynman path integrals.
In many area of mathematical physics, non-rigorous reasoning 
still plays a central part and contributes to interesting mathematics.
A: Close to he requirement in the original question: Waring's problem which generalizes Lagranges's four-square theorem. Every positive integer can be expresses as  a sum of 9 cubes, a sum of 19 fourth powers etc. For the $k$-th powers the number of summands required, denoted $g(k)$,
was a heuristic guess, $g(k) =  2^k + [ (\frac32)^k ]- 2$ and some variations of this.
Though Hilbert proved $g(k)$ is finite before 1910 actual specific values were proved decades later.  The reason I know this is because one of the persons who 'nailed the last nail into the coffin" of this problem in 1980s was working where I started my PhD.
The number of summands is very high for low numbers because (heuristically) you have only 1 and $2^k$ to use. For 4-th powers 79 is the culprit, needing fifteen 1's and four 16's.
So this lead to related another natural question: as numbers needing that many summands are small in size they may be a finite number of exceptions. Define $G(k)$  as the number of summands needed for expressing every sufficiently large integer as sum of  $k$-th powers (i.e. treat 79 as an exception for the case of fourth powers).  $G(4)$ is known to be 16. 
A: There's such a thing as "the right definition" of an intuitively defined concept.  When you state a definition and then use it in a rigorous proof, you're being rigorous, but knowing that it's the right definition is usually not rigorous.
A: It feels a bit surprising that this already has a dozen answers,
and none of them is the following fact from noncommutative algebra,
which I had thought was a canonical example of 
"non-rigorous reasoning in rigorous mathematics":
Proposition.
In a ring with identity if $1-ab$ is invertible then so is $1-ba$.
Proof: let $c = (1-ab)^{-1}$.  Then $1+bca = (1-ba)^{-1}$, because
$$
(1-ba)(1+bca) = 1 - ba + bca - babca = 1 - b(1-(1-ab)c)a = 1 - b(1-1)a = 1,
$$
and likewise
$$
(1+bca)(1-ba) = 1 - ba + bca - bcaba = 1 - b(1-c(1-ab))a = 1 - b(1-1)a = 1.
$$
Non-rigorous explanation: 
$$
c = (1-ab)^{-1} = 1 + ab + (ab)^2 + (ab)^3 + \cdots
= 1 + ab + abab + ababab + \cdots,
$$
so
$$
(1-ba)^{-1} = 1 + ba + (ba)^2 + (ba)^3 + \cdots
= 1 + ba + baba + bababa + \cdots,
$$
which can be written as
$$
1 + b(1 + ab + abab + \cdots)a = 1+bca.
$$
I don't know the original source of the Proposition and the motivation
(nor even whether the "motivation" was discovered after the fact!).
I do know that Google already guesses the right context from just
"1-ab", even before I have the chance to enter "invertible",
let alone "1-ba".  One of the top hits is this mathoverflow question
 from almost four years ago.
A: Unless I am misunderstanding, the Weil conjectures fit into this framework. I believe it took about two decades for the Grothendieck school to formalize Weil's heuristic that his conjectures follow from a Lefschetz fixed point formula for varieties over finite fields. Rather than try to flesh this post out, let me point to the Brian Osserman's article for the PCM: http://www.math.ucdavis.edu/~osserman/math/pcm.pdf. The Wikipedia account of the history also seems to be not bad (but I haven't really read it in detail): http://en.wikipedia.org/wiki/Weil_conjectures. I also seem to remember learning about the history and some of the mathematics for the first time from an article by Steven Kleiman, but cannot remember the precise reference. 
A: I think that the following "derivation" of the Prime Number Theorem from the well-known identity
$$\sum_{d\mid n}\Lambda(d) = \log n$$
is a particularly prominent example of what you are asking. Indeed, it follows from the said identity that
$$\sum_{n  \leq x} \sum_{d\mid n} \Lambda(d) = \sum_{d\leq x} \Lambda(d)\sum_{n \leq x ,\ d\mid n} 1 = \sum_{d\leq x}\Lambda(d) \left\lfloor \frac{x}{d}\right \rfloor$$
and whence,
$$\sum_{n \leq x}\Lambda(n)\left\lfloor \frac{x}{n} \right\rfloor = \sum_{n \leq x} \log n \sim x \log x.$$
Now if we replaced the $\lfloor x/n \rfloor$ in the previous line by $x/n$, we would get
$$\sum_{n\leq x}\frac{\Lambda(n)}{n} \sim \log x \sim \sum_{n  \leq x}\frac{1}{n}.$$
This might lead us to ascertain that the function $\Lambda$ of von Mangoldt behaves in the average like the arithmetical function that is identically equal to $1$, thus
$$\psi(x):=\sum_{n\leq x} \Lambda(n)\sim x.$$ 
As to the formal version of the preceding argument you may want to take a look at sections 9.9 through 9.12 of [2]. You are to find there a proof of the Prime Number Theorem (presumably due to Ingham) based on the estimate
$$\sum_{n \leq x} \psi\left(\frac{x}{n}\right) = x\log x - x+ O(\log x), \quad x \geq 1.$$
According to Prof. Balanzario (see [1, page 59]): "This demonstration ... is the correct version of our heuristic reasoning [given above]." 
References
[1] E. P. Balanzario. Breviario de Teoría Analítica de los Números. SMM, México, 2003. 
[2] W. Rudin. Functional Analysis. Tata McGraw Hill Publishing Company Ltd., 1974.
A: Have you reads Proofs and Refutations by Lakatos?  It's all about the dynamic tension between "heuristics" (don't get mad at me, Andrew Stacey!) and rigorous proof, centering particularly on a classroom situation where they are discussing Euler's formula V - E + F = 2. The difference between the first attempted "proofs" or thought experiments and the final rigorous proof involving homology is pretty stark; the first proof is however memorable and explanatory.
Even in pre-Robinson days before they were made rigorous, you could say that the original intuitions of infinitesimals in calculus were effective and explanatory (even today, I am told, among certain physicists and engineers who might never learn the rigorous foundations). If you read the introduction to Models of Smooth Infinitesimal Analysis by Moerdijk and Reyes, you will see examples of intuitive reasoning with infinitesimals among geometers like Lie and E. Cartan which were certainly convincing to them, but which had to undergo some distortion to meet the demands of Weierstrassian rigor -- at least that was so until recent years when the types of reasoning with nilpotent infinitesimals in smooth analysis were clarified and made rigorous through sheaf theory and its internal logic. 
A: George Pólya wrote some classic books on this topic, especially his two-volume set Mathematics and Plausible Reasoning: Vol. I, Induction and Analogy in Mathematics, and Vol. II, Patterns of Plausible Inference.
A: In number theory, there are many probabilistic arguments regarding prime numbers that give the right answer, even though they are not rigorous. For example, you can "derive" the prime number theorem by arguing that a fixed large number $n$ has probability $1/p$ of being divisible by $p$, and then finding the prime distribution that gives the right balance.
Terry Tao has discussed this topic in his blog:
254A, Supplement 4: Probabilistic models and heuristics for the primes (optional)
The probabilistic heuristic justification of the ABC conjecture
A: There is a well known connection between parabolic and elliptic partial differential equations and Brownian motion.  By now it very well explored formally (e.g. the probabilistic proof of Hörmander's theorem due to Malliavin) but it used to be the case that people would get their intuition from Brownian motion and then prove a theorem by completely different means.
One example is the following quote from Nash's 1958 paper "Continuity of solutions of parabolic and elliptic equations":

The methods here were inspired by physical intuition, but the ritual of mathematical exposition tends to hide this natural basis.  For parabolic equations, diffusion, Brownian movement, and flow of heat or electrical charge all provide helpful interpretations.

As a side note.  One of the people who contributed the most to establishing the formal connection between Brownian motion and parabolic/elliptic equations was Joseph Doob.  He had done his Phd. thesis on harmonic analysis, but couldn't find a job anywhere (this was a couple of years after the Great Depression) until he got offered a post at a probability department.  He started working on formal (i.e. Kolmogorov) foundations of probability and ended up establishing the connection between harmonic functions and Martingales.  He's one of my favorite mathematicians and I think his contributions are underrated.
A: I feel that almost all of math is this way. One specific example is the Riemann mapping theorem for annuli (which is equivalent to the standard Riemann mapping theorem). Riemann is said to have conceived of the idea by imagining current flowing from the inside of an annulus to the outside. The current flows and equipotentials would form an orthogonal set of coordinates which could be "stretched out" to form a perfect cylinder. Riemann's first proof of this theorem was shown to have an error, but he reportedly commented that it didn't matter, because he knew the theorem was true anyway. (Most of this comes from Jim Cannon's paper The Combinatorial Riemann Mapping Theorem). 
