Worked solution: Flyspeck: a formal proof of the Kepler conjecture in HOL Light and Isabelle (2015)

Step 6 of 9: Certify infeasibility of every linear program with a verified dual solution

In plain words

To convince a skeptical machine that a system of linear inequalities has no solution, it's not enough to say 'I tried and failed' — you must hand over a short recipe (a set of non-negative weights) that combines the inequalities into an obviously false statement like $0 \le -1$ ; checking that recipe is just adding numbers, which a proof assistant trusts completely, unlike the external numerical solver that first guessed the recipe.

\lambda \ge 0, \quad \textstyle\sum_i \lambda_i\,(\text{constraint}_i) \;\Longrightarrow\; 0 \le -\varepsilon \ \ (\varepsilon>0)

Detailed analysis

Infeasibility of a linear program is checked by exhibiting nonnegative multipliers $\lambda$ for its constraints whose weighted sum collapses every variable and yields a plainly false inequality such as $0 \le -\varepsilon$ — a Farkas-style dual certificate that a formal proof can check by pure arithmetic, without re-solving the program. About half of the roughly $18\,762$ tame graphs need their feasible region split into several sub-cases (by branching on inequalities like $x \le a$ or $a \le x$ ) before a linear relaxation is tight enough to be infeasible, and irrational coefficients such as $\sqrt2$ or $\pi$ are replaced by verified rational bounds. In total $43\,078$ linear programs are generated and every one is formally certified infeasible.

Terms in this step

dual certificate (Farkas certificate): A set of non-negative multipliers, one per inequality, whose weighted sum of the inequalities collapses to a statement that is plainly false; its existence is a rigorous proof that the original system has no solution, and it can be checked by simple arithmetic instead of by re-solving the system.

Knowledge used in this step

Linear programming

Common mistake. The external solver GLPK is used only to search for candidate dual multipliers, and its floating-point output need not be trustworthy; the formal HOL Light proof re-derives a corrected, exact-arithmetic dual certificate from that guess and checks it by hand-verifiable summation, so no numerically unreliable step ever enters the kernel of the proof.