Editing Four color theorem (section)

===Simplification and verification===
Since the proving of the theorem, a new approach has led to both a shorter proof and a more efficient algorithm for 4-coloring maps. In 1996, [[Neil Robertson (mathematician)|Neil Robertson]], [[Daniel P. Sanders]], [[Paul Seymour (mathematician)|Paul Seymour]], and [[Robin Thomas (mathematician)|Robin Thomas]] created a [[polynomial time|quadratic-time]] algorithm (requiring only [[Big O notation|O]](''n''<sup>2</sup>) time, where ''n'' is the number of vertices), improving on a [[quartic function|quartic]]-time algorithm based on Appel and Haken's proof.<ref>{{harvtxt|Thomas|1995}}; {{harvtxt|Robertson|Sanders|Seymour|Thomas|1996}}.</ref> The new proof, based on the same ideas, is similar to Appel and Haken's but more efficient because it reduces the complexity of the problem and requires checking only 633 reducible configurations. Both the unavoidability and reducibility parts of this new proof must be executed by a computer and are impractical to check by hand.{{sfnp|Thomas|1998|pp=852–853}} In 2001, the same authors announced an alternative proof, by proving the [[snark conjecture]].<ref>{{harvtxt|Thomas|1999}}; {{harvtxt|Pegg|Melendez|Berenguer|Sendra|2002}}.</ref> This proof remains unpublished, however.

In 2005, [[Benjamin Werner]] and [[Georges Gonthier]] formalized a proof of the theorem inside the [[Coq (software)|Coq]] proof assistant. This removed the need to trust the various computer programs used to verify particular cases; it is only necessary to trust the Coq kernel.{{sfnp|Gonthier|2008}}