Only yesterday I read this digression in Girard's The Blind Spot:

Once in a while I would like to indulge into an anecdote concerning the genesis of the proof. The criterion was found by the end of 1985; then I remained more than six months making circles around the "splitting tensor". One nice day of August 1986, I woke up in a camping of Siena and I had got the proof: I therefore sat down and wrote a manuscript of 10 pages. One month later, I was copying this with a typewriter, and I discovered that one of my lemmas was wrong: no importance, I made another lemma! This illustrates the fact, neglected by the formalist ideology, that a proof is not putting side by side logical rules, it is a global perception: since I had found the concept of empire, I had my theorem and the faulty lemma was no more than a misprint.