 One currently active area of work that has led to the uncovering of hitherto unrecognized gaps of various sorts is automated proof checking. Specially designed computer programs are used to check the validity of proofs that have been rendered in an appropriate formal language. The main focus thus far has not been on discovering new results but on checking the status of proofs of already established results. George Gonthier has used this approach to verify a proof of the four color theorem (Gonthier 2008) and a proof of the odd order theorem in group theory (Gonthier et al. 2013), and Thomas Hales has verified a proof of the Jordan curve theorem (Hales 2007). In each case, a number of gaps were found and then traversed. Formal verification of this sort can also reveal other information hidden in the content of ordinary mathematical arguments. Georg Kreisel has described this general process as “unwinding proofs”, while Ulrich Kohlenbach has more recently coined the term “proof mining.” In connection with the methods described above, Avigad writes that