ing of spheres is the densest possible.
This proof, in addition to involving
extensive case enumerations at different levels, is also very complicated in
the interaction between the various
parts. In August 2014, a team headed
by Hales announced the completion
of the Flyspeck project, constructing a
formal proof of Kepler’s conjecture. 16
Yet another example is the proof by
Tucker30 for Lorenz’s conjecture (
number 14 in Smale’s list of challenging
problems for the 21st century). The
conjecture states that Lorenz’s system
of three differential equations, providing a model for atmospheric convection, supports a strange attractor.
Tucker (page 104) 30 described the run
of a parallel ODE solver several times
on different computer setups, obtaining similar results.
Certified Computation. This technique is based on the idea it may be
easier to check a given answer for correctness than come up with such an
answer from scratch. The prototype
example is the solution of an equation like 3x3 − 4x2 − 5x + 2 = 0. While
it may be a challenge to find the solution x = 2, it is straightforward to substitute the solution into the equation
and check whether it is fulfilled. The
result is trustworthy not because it is
accompanied by a formal proof but
because it is so simple to check, much
simpler than the algorithm (perhaps
Newton iteration in this case) used to
solve the problem in the first place.
In addition to the solution itself, it
may be required that a certifying algorithm provide a certificate in order
to facilitate the checking procedure. 25
Developing such certificates and computing them without excessive overhead may require algorithmic innovations (see the first sidebar “Certified
Computations”).
In our case, the result computed
by our program can be interpreted
as the eigenvalue of a giant matrix
Q, which is not explicitly stored but
implicitly defined through an iteration procedure. The certificate is a
vector v that is a good-enough approximation of the corresponding eigenvector. From this vector, one can
compute certified bounds on the eigenvalue in a rather straightforward
way by comparing the vector v to the
product Qv.
These two approaches comple-
ment each other; a simpler check-
ing procedure is more amenable to a
formal proof and verification proce-
dure. However, we did not go to such
lengths; a formal verification of the
program would have made sense only
in the context of a full verification that
includes also the human-readable
parts of the proof. We instead used
traditional methods of ensuring pro-
gram correctness of the certificate-
checking program.
Twisted Cylinders
A “twisted cylinder” is a half-infinite
wraparound spiral-like square lattice
(see Figure 3). We denote the perim-
A certifying algorithm not only produces the result but also justifies its correctness by
supplying a certificate that makes it easy to check the result. In contrast with formally
verified computation, correctness is established for a particular instance of the
problem and a concrete result. Here, we illustrate this concept with a few examples; see
the survey by McConnell et al. 25 for a thorough treatment.
The greatest common divisor. The greatest common divisor of two numbers can be
found through the ancient Euclidean algorithm. For example, the greatest common
divisor of 880215 and 244035 is 15. Checking that 15 is indeed a common divisor is
rather easy, but not clear is that 15 is the greatest. Luckily, the “extended” Euclidean
algorithm provides a certificate: two integers p = −7571 and q = 27308, such that
880215p + 244035q = 15. This proves any common divisor of 880215 and 244035 must
divide 15. No number greater than 15 can thus divide 880215 and 244035.
Systems of linear equations and inequalities. Consider the three equations 4x − 3y
+ z = 2, 3x − y + z = 3, and x − 7y – z = 4 in three unknowns x, y, z. It is straightforward
to verify any proposed solution; however, the equations have no solution. Multiplying
them by 4, − 5, − 1, respectively, and adding them up leads to the contradiction 0 = − 11.
The three multipliers thus provide an easy-to-check certificate for the answer. Such
multipliers can always be found for an unsolvable linear system and can be computed
as a by-product of the usual solution algorithms. A well-known extension of this
example is linear programming, the optimization of a linear objective function subject
to linear equations and inequalities, where an optimality certificate is provided by the
dual solution.
Testing a graph for 3-connectedness. Certifying that a graph is not 3-connected is
straightforward. The certificate consists of two vertices whose removal disconnects the
graph into several pieces. It has been known since 1973 that a graph can be tested for
3-connectedness in linear time, 17 but all algorithms for this task are complicated. While
providing a certificate in the negative case is easy, defining an easy-to-check certificate
in the positive case and finding such a certificate in linear time has required graph-theoretic and algorithmic innovations. 28 This example illustrates that certifiability
is not primarily an issue of running time. All algorithms, for constructing, as well
as for checking, the certificate, run in linear time, just like classical non-certifying
algorithms. The crucial distinction is that the short certificate-checking program is by
far simpler than the construction algorithm.
Comparison with the class NP. There is some analogy between a certifying
algorithm and the complexity class NP. For membership in NP, it is necessary only
to have a certificate by which correctness of a solution can be checked in polynomial
time. It does not matter how difficult it is to come up with the solution and find the
certificate. In contrast with a certifying algorithm, the criterion for the checker is not
simplicity but more clear-cut—running time. Another difference is that only “positive”
answers to the problem need to be certified.
Certified Computations
Figure 3. A twisted cylinder of perimeter W = 5.
W = 5
1
3
4
5
6
7
8
2
2