Cutting Planes with Lean 4

This project follows the research in Lean 4 Theorem Proving and Metaprogramming, where we where we aim to develop a Lean 4 library for formalizing and manipulating cutting planes in a verifiable manner, as they were described by Jakob Nordström in A Unified Proof System for Discrete Combinatorial Problems.

This work bridges the gap between the theoretical underpinnings of cutting planes—a mathematical optimization technique used in linear programming to refine solution spaces—and the rigorous environment of theorem proving offered by Lean 4. Our goal is to model the foundational concepts of cutting plane calculation, implement these calculations' rules, and formally verify their correctness.

By Bernardo Borges as a capstone project for the Bachelor's degreen in Computer Science at Universidade Federal de Minas Gerais.

Documentation

This manual is generated by mdBook.

You can read the docs here.

Run mdbook test to test all lean code blocks.

Work Progress

• Addition proof
• Multiplication proof
• Saturation proof
• Division proof
• Test cases
• Documentation

Example

We want to represent Pseudo-Boolean formulas to decide whether they are satisfiable. For instance,

$$ \overline x_1 + 2x_2 + 3\overline x_3 + 4x_4 + 5\overline x_5 \ge 1 $$

will be represented as

open PseudoBoolean

variable {xs : Fin 5 → Fin 2}

def my_pb : PBIneq ![(0,1),(2,0),(0,3),(4,0),(0,5)] xs 1 := ...

This notation is under development and is subject to changes.

Now we can manipulate PBs, similarly to this Toy Example:

variable {xs : Fin 4 → Fin 2}

--                       w     x     y     z
example (c1 : PBIneq ![(1,0),(2,0),(1,0),(0,0)] xs 2)
        (c2 : PBIneq ![(1,0),(2,0),(4,0),(2,0)] xs 5)
        (c3 : PBIneq ![(0,0),(0,0),(0,0),(0,1)] xs 0)
  : PBIneq ![(1,0),(2,0),(2,0),(0,0)] xs 3
  := by
  let t1 : PBIneq ![(2,0),(4,0),(2,0),(0,0)] xs 4  := by apply Multiplication c1 2
  let t2 : PBIneq ![(3,0),(6,0),(6,0),(2,0)] xs 9  := by apply Addition t1 c2
  let t3 : PBIneq ![(0,0),(0,0),(0,0),(0,2)] xs 0  := by apply Multiplication c3 2
  let t4 : PBIneq ![(3,0),(6,0),(6,0),(0,0)] xs 7  := by apply Addition t2 t3
  exact Division t4 3
  done