the idea of local analysis, were developed further into tools used in the classification. Perhaps the most revolutionary aspect of the proof was its length: before the Feit–Thompson paper, few arguments in group theory were more than a few pages long and most could be read in a day. Once group theorists realized that such long arguments could work, a series of papers that were several hundred pages long started to appear. Some of these dwarfed even the Feit–Thompson paper; the paper by Michael Aschbacher and Stephen D. Smith on quasithin groups was 1,221 pages long. Revision of the proof Many mathematicians have simplified parts of the original Feit–Thompson proof. However all of these improvements are in some sense local; the global structure of the argument is still the same, but some of the details of the arguments have been simplified. The simplified proof has been published in two books: , which covers everything except the character theory, and , which covers the character theory. This revised proof is still very hard, and is longer than the original proof, but is written in a more leisurely style. A fully formal proof, checked with the Coq proof assistant, was announced in September 2012 by Georges Gonthier and fellow researchers at Microsoft Research and INRIA. An outline of the proof Instead of describing the Feit–Thompson theorem directly, it is easier to describe Suzuki's CA theorem and then comment on some of the extensions needed for the CN-theorem and the odd order theorem. The proof can be broken up into three steps. We let G be a non-abelian (minimal) simple group of odd order satisfying the CA condition. For a more detailed exposition of the odd order paper see or or . Step 1. Local analysis of the structure of the group G This is easy in the CA case because the relation "a commutes with b" is an equivalence relation on the non-identity elements. So the elements break up into equivalence classes, such that each equivalence class is the set of non-identity elements of a maximal abelian subgroup. The normalizers of these maximal abelian subgroups turn out to be exactly the maximal proper subgroups of G. These normalizers are Frobenius groups whose character theory is reasonably transparent, and well-suited to manipulations involving character induction. Also, the set of prime divisors of |G| is partitioned according to the primes which divide the orders