HEXAGONbeta

A Verified Constructive Reduction of the Cook-Levin Theorem in Lean 4: Bridging the Gap Between Complexity Theory and Formal SAT Encodings

A mix of human-written and AI-generated textHuman understanding: all partscs.CC โ€” Computational Complexitymath.LO โ€” Logiccs.DM โ€” Discrete Mathematicscs.FL โ€” Formal Languages and Automata Theorycs.LO โ€” Logic in Computer Science

Contributed by Jonathan ๐‘“(n) Reed โ†—

Version 1 / Oct 08, 2026 / CC BY 4.0

Abstract

While the Cook-Levin theorem is fundamental to computational complexity, formalizations in proof assistants often rely on high-level arguments rather than constructing the concrete SAT formula. Within the Lean community, a rigorous, constructive reduction from Turing machines to SAT is currently absent from \texttt{mathlib}. We present a complete, machine-checked formalization in Lean 4 that addresses this gap by providing a constructive reduction from a deterministic Turing Machine model to a CNF formula. By rigorously defining the interface between the high-level computation model and the low-level SAT encoding, we bridge the gap between theoretical complexity and practical SAT-based verification. Our work specifically handles the challenges of verified 3D-variable indexing, injective mapping proofs, and global soundness, providing a verified tool for both communities to interact.

Provenance statement

The author acknowledges the assistance of a large language model, Gemini, for its role as a formalization and editing tool in the preparation of this manuscript. The AI was used under the direct control of the author. All intellectual and creative decisions, as well as final editorial responsibility, rest with the author.

Tools used

Google
Gemini
Lean
LeanVersion v4.28.0

References

  1. Biere, A., Heule, M., van Maaren, H.: Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications (2009)
  2. Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the third annual ACM symposium on Theory of computing. pp. 151--158 (1971)
  3. de Moura, L., Ullrich, S.: The Lean 4 Programming Language and Theorem Prover. In: International Conference on Automated Deduction. pp. 625--635. Springer (2021)
  4. Levin, L.: Universal search problems. Problems of Information Transmission 9(3), 115--129 (1973)
  5. Sipser, m.: Introduction to the Theory of Computation. Cengage Learning (2012)

Version history

  1. v1Submitted by Jonathan ๐‘“(n) ReedInitial depositCurrentOct 07, 2026