Marijn Heule translates mathematical conjectures into satisfiability problems — logical formulas with millions of variables and clauses — and feeds them to SAT solvers. The solver either finds a satisfying assignment (a counterexample to the conjecture) or proves that none exists (confirming the conjecture). The method cracked the Keller conjecture in dimension 7, a problem open for 90 years.
The proof is 200 terabytes. No human can read it. No human can check it by hand. Verification requires running another program — a proof checker — that traces the solver's logical steps and confirms each one follows from the axioms. The proof is correct, but it is correct in a way that no person can directly understand.
This creates a new category of mathematical knowledge: theorems that are true, verified, and opaque. The statement of the Keller conjecture is simple — it asks whether certain tilings of space must contain pairs of cubes that share a face. The proof that the conjecture fails in dimension 7 is not simple. It is a computational artifact that encodes an exhaustive search through a combinatorial space too large for human comprehension. The search was conducted correctly. The result is trustworthy. But the reason the conjecture fails — the structural insight that would explain why dimension 7 is the critical threshold — is not present in the proof. The proof says “it fails” without saying “here is why it fails.”
Heule's program is not the first instance of computer-assisted proof. The four-color theorem (1976) and Kepler conjecture (2014) both required computational verification. But SAT solving differs in scale and generality. The method is not specific to graph coloring or sphere packing. It is a general-purpose technique: any mathematical statement that can be encoded as a finite logical formula can, in principle, be attacked this way. The constraint is not the method's applicability but the encoding's size — whether the resulting formula fits in available memory and can be solved in available time.
The philosophical question is whether this counts as understanding. Mathematics has traditionally been a discipline where proof and insight are entangled — you prove a theorem by understanding why it's true, and the proof communicates that understanding to others. SAT proofs sever this connection. The theorem is proved. The understanding is absent. The mathematical community can use the result — build on it, apply it, cite it — but cannot learn from the proof the way they learn from a proof by Euler or Ramanujan.
The counterargument is that proof has always been more mechanical than mathematicians like to admit. Formal proofs in any system are sequences of syntactic manipulations; the “insight” is in the human presentation, not the logical content. SAT solving just makes the mechanical nature explicit. But this undersells the difference. A proof by a human mathematician, even when formalized, typically contains structures — lemmas, constructions, analogies — that compress the argument and make it navigable. A 200-terabyte SAT proof has no such structure. It is flat. The information is all there, but the compression is absent, and the compression is what understanding means.