# LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean

arXiv: https://arxiv.org/abs/2607.28459 · HTML: https://mlsanity.com/paper/2607.28459/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 47 references that are in the map.
- First posted on arXiv 30 Jul 2026.

## Builds on (most cited first, 12 of 12)

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs](https://mlsanity.com/paper/2209.12185/) (2022)
- [Efficient Certified RAT Verification](https://mlsanity.com/paper/1612.02353/) (2016)
- [Certified Symmetry and Dominance Breaking for Combinatorial Optimisation](https://mlsanity.com/paper/2203.12275/) (2022)
- [Lean-SMT: An SMT tactic for discharging proof goals in Lean](https://mlsanity.com/paper/2505.15796/) (2025)
- [Lean4Lean: Verifying a Typechecker for Lean, in Lean](https://mlsanity.com/paper/2403.14064/) (2024)
- [Formalising the h-principle and sphere eversion](https://mlsanity.com/paper/2210.07746/) (2022)
- [Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing](https://mlsanity.com/paper/2004.05934/) (2020)
- [Formal Verification of the Empty Hexagon Number](https://mlsanity.com/paper/2403.17370/) (2024)
- [Formally Verified SAT-Based AI Planning](https://mlsanity.com/paper/2010.14648/) (2020)
- [Formally Verified Transformation of Non-binary Constraints into Binary Constraints](https://mlsanity.com/paper/2009.00583/) (2020)
- [PBLean: Pseudo-Boolean Proof Certificates for Lean 4](https://mlsanity.com/paper/2602.08692/) (2026)

## Abstract (arXiv)

Constraint programming is a core technology for solving complex combinatorial problems in scheduling, planning, configuration, and verification. Trusting its results therefore demands guarantees at two levels: that reformulations applied beforehand are semantics-preserving, and that solvers produce correct answers. In this work, we introduce a framework that addresses both verification levels in the Lean theorem prover: it can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families; and to check solver-produced certificates for individual instances via translation backends to external formats such as MiniZinc, SMT-LIB, and OPB. Combining both levels yields an end-to-end workflow that establishes the satisfiability or unsatisfiability of a constraint problem without trusting the external solver. Experimental results show that our framework's verified symmetry breaking also pays off in practice: a single parametric proof per problem family, reused across all instance sizes, reduces solver search effort by a factor of up to 2x10^7, while the entire in-Lean certification stays affordable, taking at most a few minutes for our largest instances.