Mathematics & Theoretical Computer Science
When OR Algorithms Proved Mathematical Theorems
Three landmark results where Linear Programming, Branch-and-Bound, and SAT solvers crossed from engineering tools into the realm of pure mathematics — settling conjectures that had resisted human proof for centuries.
Landmark Results
Select a theorem to explore its history, formulation, and interactive solver
Historical Context
In 1852, Francis Guthrie noticed that four colors sufficed to color a map of England's counties so that no two adjacent counties shared the same color. He asked whether this held for every possible map. For 124 years, the conjecture resisted proof despite attempts by Kempe (1879, later shown flawed), Birkhoff, and many others.
In 1976, Kenneth Appel and Wolfgang Haken at the University of Illinois produced the first computer-assisted proof in mathematics. They reduced the infinite set of planar maps to 1,936 reducible configurations, each verified by roughly 1,200 hours of computer time on an IBM 370. The proof was deeply controversial — many mathematicians rejected it because no human could verify every case by hand. In 1997, Robertson, Sanders, Seymour, and Thomas streamlined the argument to 633 configurations with a cleaner program.
The Problem. Coloring a planar graph with the minimum number of colors such that no two adjacent vertices share a color is NP-hard in general. The Four Color Theorem states that every planar graph is 4-colorable. The proof works by showing that any minimal counterexample must contain one of a finite set of reducible configurations — and then showing computationally that each configuration can be reduced, producing a contradiction.
subject to
Σc xic = 1 ∀ i ∈ V // each vertex gets exactly one color
xic + xjc ≤ 1 ∀ (i,j) ∈ E, ∀ c // adjacent vertices differ
xic ≤ yc ∀ i, c // color c used only if activated
xic, yc ∈ {0, 1}
Interactive Graph Coloring
| Algorithm | Colors Used | Conflicts | Optimal? |
|---|
Key References
Historical Context
In 1611, Johannes Kepler conjectured that the densest way to pack identical spheres in three dimensions is the face-centered cubic (FCC) arrangement, achieving a packing density of π/√18 ≈ 74.05%. For 387 years, the conjecture remained unproved despite contributions from Gauss, Thue, and Fejes Tóth.
In 1998, Thomas Hales announced a proof that relied on a massive computational verification. He partitioned space into Voronoi cells around each sphere center and showed that the local density of every possible arrangement is bounded by the FCC density. The proof required solving over 150,000 linear programming instances. The referees spent four years and declared themselves 99% certain. Hales then launched the Flyspeck project (2003–2014) to produce a formal, machine-verified proof in HOL Light and Isabelle, which was completed in 2014 and published in 2017.
The Problem. Kepler's conjecture concerns the optimal packing of spheres in 3D space. Hales' proof strategy reduces the global problem to a finite set of local arrangements. For each arrangement, an LP relaxation bounds the score function that measures how efficiently spheres fill space. If every LP solution is at most the FCC score, the conjecture holds.
Proof method:
1. Partition R³ into Voronoi cells around sphere centers
2. Define score function σ(D) for each Delaunay star D
3. For each of ~5,000 tame graphs G:
solve LP: max σ(D) s.t. geometric constraints
// ~150,000 LP instances total
4. Verify σ*(G) ≤ 8 pt ≈ 4.266 for all G
5. Flyspeck: formal verification in HOL Light + Isabelle
2D Circle Packing Explorer
| Metric | Value |
|---|
Key References
Historical Context
Ramsey theory guarantees that sufficiently large structures must contain ordered substructures. The Ramsey number R(s,t) is the smallest n such that every 2-coloring of the edges of the complete graph Kn contains either a red Ks or a blue Kt. The classic result R(3,3) = 6 is elegant: K5 can be 2-colored without a monochromatic triangle, but K6 cannot.
Computing Ramsey numbers is extraordinarily hard. R(4,5) = 25 was established by McKay and Radziszowski in 1995 through exhaustive Branch-and-Bound search requiring massive computation. The value of R(5,5) remains unknown; the best bounds are 43 ≤ R(5,5) ≤ 48. Erdős famously said that if aliens demanded we compute R(5,5) or face destruction, we should devote all resources to computation — but for R(6,6), we should prepare for war.
The Problem. Lower bounds on R(s,t) are found by constructing a 2-coloring of Kn-1 with no monochromatic Ks in red and no Kt in blue. Upper bounds require exhaustive verification that no such coloring exists for Kn. Both directions use ILP, local search, and Branch-and-Bound.
R(3,4) = 9 // Greenwood & Gleason 1955
R(3,5) = 14 // Graver & Yackel 1968
R(4,4) = 18 // Greenwood & Gleason 1955
R(4,5) = 25 // McKay & Radziszowski 1995 (B&B)
43 ≤ R(5,5) ≤ 48 // open problem
Lower bound: Find 2-coloring of Kn-1 with no mono-Ks (ILP/search)
Upper bound: Prove no such coloring exists for Kn (exhaustive B&B)
Ramsey Number Explorer
| Result | Details |
|---|
Key References
Explore More OR Applications
From scheduling and routing to packing and network design, see how mathematical optimization solves real-world problems across industries.