Introduction

Cutting Planes and Lean 4

Cutting Planes is a method in mathematical optimizaiton used in the context of discrete combinatorial problems, that can be applied in Software testing, Formal verification and Proof logging. Pseudo-Boolean in the other hand is a logic system introduced by Jakob Nordström in his paper A Unified Proof System for Discrete Combinatorial Problems, which this project aims to implement and verify. Our proofs will consist of Pseudo-Boolean Constraints, that are 0-1 integer linear inequalities. Without loss of generality, we will use the normalized form.

\[ \sum_i{a_i l_i} \ge A \] Where we have:

• constant \( A \in \mathbb{N} \)
• coefficients \( a_i \in \mathbb{N} \)
• literals \( l_i: x_i\ \text{or}\ \overline{x_i}\ (\text{where } x_i + \overline{x_i} = 1) \)
• variables \( x_i \) take values \( 0 = false \) or \( 1 = true \)

In this regard, Pseudo-Boolean Reasoning works on two axioms and four rules, each of which are formally verified in this project using Lean 4

Lean 4 is a theorem prover and programming language developed by Leonardo de Moura. In the last years it became proeminent in the mathematics community, after Kevin Buzzard's The Xena Project of Imperial College London was formed, aiming to formalize all undergraduate level math, Peter Scholze's proof in the area of condensed mathematics called Liquid Tensor Experiment was formalized in 2021 and in 2023 Terence Tao used Lean to formalize a proof of the Polynomial Freiman-Ruzsa (PFR) conjecture, published in the same year.

Armed with a Lean 4 proof of the reasoning rules, complex proofs that involve these steps can be guaranteed to be correct.