Pith. sign in

REVIEW 2 major objections 5 minor 48 references

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

T0 review · 2 major / 5 minor · reviewed 2026-07-31 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A Lean framework proves constraint reformulations once for whole problem families and checks external solvers so you get end-to-end (un)satisfiability theorems without trusting the solver.

desk verdict Shipped Lean pipeline that actually attaches certificates to high-level CSPs and parametric reformulations—not just low-level formulas—with honest TCB and real SBC payoff numbers. read the letter →

arxiv 2607.28459 v1 pith:M344AYBG submitted 2026-07-30 cs.AI cs.LO

Pablo Manrique , Stefan Szeider This is my paper
classification cs.AIcs.LO
keywords constraintsatisfactionLeantheoremproversymmetrybreakingproofcertificatesequisatisfiabilitypseudo-Booleanproofsformalverificationprogramming
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Constraint solvers are widely used but hard to trust: reformulations (especially symmetry breaking) can silently drop solutions, and the solvers themselves can be buggy. LeanCSP lets you write a constraint problem in Lean, prove once and for all that two formulations are equivalent or equisatisfiable (including that a symmetry-breaking constraint is sound) for every instance size in a family, then hand a concrete instance to an external solver and check its SAT or UNSAT certificate back inside Lean. The external solver and the file translations sit outside the trusted base; a successful check yields a Lean theorem about the original CSP. The paper shows this pipeline can certify results such as S(4)=44, and that a single parametric symmetry proof can cut solver search by up to about 20 million times while full in-Lean checking stays on the order of minutes.

What carries the argument

Parametric π-equivalence and domain/variable symmetry-breaking constraints in Lean, combined with a library of 40+ constraints whose CSP-to-PB encoding is proved sound, so a checked VeriPB certificate against the in-Lean PB model implies unsatisfiability of the original CSP.

What would settle it

Exhibit a library CSP whose Lean model is accepted and certified unsatisfiable (or satisfiable) but that disagrees with the standard mathematical statement of the same combinatorial problem, or a soundness gap in the CSP-to-PB theorems that lets a satisfiable CSP produce a checked UNSAT certificate.

Watch

Extended reading notes

Core claim

LeanCSP is presented as the first end-to-end formally verified pipeline for a general constraint language: a CSP written in Lean is taken as the problem specification, reformulation properties (equivalence, equisatisfiability, symmetry-breaking soundness) are proved parametrically for whole families, and instance certificates from external solvers are checked back against that CSP (via a sound CSP-to-pseudo-Boolean translation and PBLean for UNSAT), so neither the translation nor the solver need be trusted.

Load-bearing premise

The CSP written in Lean is treated as the true mathematical specification of the problem; if that model is wrong about the intended question, the certificates only prove facts about the model.

Editorial extensions

If this is right

  • A single parametric symmetry or equivalence proof can be reused for every instance size, turning one-time proof effort into repeated solver speedups (measured up to ~2×10^7 in deterministic operations).
  • Combinatorial bounds such as S(4)=44, R(3,3)≤6, and W(2,3)≤9 can be stated as ordinary Lean theorems whose proofs go through external search plus in-Lean certificate checking.
  • Unsound reformulations that pass testing on small n (e.g. a reversal leader on ordinary Schur that only fails at n=13) are refused because the required family-level symmetry proof cannot be given.
  • Full in-Lean certification of the largest reported instances stays within a few minutes, so the trusted check is practical relative to solving.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same pattern—parametric reformulation proofs plus reflected certificate checking—could be applied to other CP global constraints or to optimization (not only decision) if dominance proofs are wired in the same way.
  • Because the Lean CSP is the specification, library growth and modeling discipline become the main remaining sources of error; community libraries of verified encodings would amplify the approach.
  • Choosing pseudo-Boolean certificates over SAT was driven by compact cutting-planes proofs on counting problems; families outside that regime may still prefer a SAT/LRAT path once fully wired.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper introduces LeanCSP, a Lean 4 framework that addresses two verification needs in constraint programming: (i) parametric proofs of reformulation properties—equivalence via π-equivalence, equisatisfiability, and soundness of variable/domain symmetry-breaking constraints—for entire CSP families built from a library of 40+ constraints; and (ii) instance-level certification of external solver answers by translating Lean CSPs to MiniZinc, SMT-LIB, or OPB, then checking SAT witnesses directly and UNSAT VeriPB proofs via PBLean against a soundness-proved CSP-to-PB encoding. Combining both layers yields end-to-end Lean theorems (e.g., schur_4_exact establishing S(4)=44) without trusting solvers or unverified translations. Experiments compare PB vs SAT proof scaling, measure verified SBC speedups up to ~2×10^7 in deterministic operations, and show in-Lean certification costs of at most a few minutes on the largest instances.

Significance. If the development is as claimed, this is a substantial systems contribution to trustworthy combinatorial solving: a general, library-uniform end-to-end pipeline inside a modern ITP, with parametric family-level reformulation proofs rather than per-instance certificates alone. Strengths that should count explicitly include the shipped Lean development and public code, machine-checked CSP-to-PB soundness for the library, the cautionary Schur reversal example that the framework refuses rather than silently accepts, concrete Lean theorems for classical bounds (S(4), R(3,3), W(2,3)), honest experimental reporting (including cases where SBCs do not help), and clear disclosure that the Lean CSP is taken as specification and that PBLean reflection adds Lean.ofReduceBool/Lean.trustCompiler to the TCB. The work cleanly separates formulation-level guarantees from solver certificates and is a natural foundation for further certified CP/SMT work in Lean.

major comments (2)
  1. [Section 3] Section 3 (TCB and specification paragraph): The central pipeline claim is sound as stated, but the manuscript should state more prominently—ideally in the abstract or introduction, not only mid-Section 3—that end-to-end theorems are theorems about the Lean CSP model taken as specification, and that the trusted base includes the Lean kernel plus the two reflection/compiler axioms used by PBLean. This is standard for the genre and already disclosed, but it is load-bearing for how readers will cite the S(4)=44-style results; a short explicit TCB box or paragraph would prevent over-reading the guarantees as theorems about an independent mathematical ground truth.
  2. [Section 3] Section 3 and library scope: UNSAT lifting rests on per-constraint CSP-to-PB soundness for the fixed library. The paper should state more sharply what happens when a user adds a new DynamicConstraint outside that library (no automatic UNSAT path until a new soundness lemma is proved), and whether the MiniZinc/SMT SAT path still applies unchanged. This does not break the main claim for library CSPs, but it bounds the “uniformly for every CSP built from our library” slogan and should be explicit so the contribution is not overstated.
minor comments (5)
  1. [Table 1, Table 2] Table 1 and Table 2: Consider adding a one-line note that Equiv./SB line counts are human proof effort (not generated), and that geo. mean speedups exclude Schur’s unsolved-without-SBC largest point as already footnoted—make the exclusion rule visible in the table caption itself.
  2. [Figure 2, Section 4] Figure 2: The odd-cycle panel supports the “gap is resolution, not encoding” reading; a sentence in §4 stating the CNF encoding used for the SAT baseline (and whether cardinality was encoded naively) would make the comparison fully reproducible from the text alone.
  3. [Section 1] Related work: A slightly sharper contrast with Dubois (2020) on verified non-binary-to-binary transformations and with VeriPB dominance/symmetry logging (Bogaerts et al., 2023) would help readers place the parametric Lean proofs versus instance-level proof logging; the distinction is present but could be one tighter paragraph.
  4. Presentation: The submitted text has many run-together words (likely PDF extraction artifacts, e.g., “formulation-levelproperties”, “2×10 7”). Ensure the camera-ready source has clean spacing and that code listings match the repository identifiers exactly.
  5. [Example 4] Example 4 / schur_4_exact: Mention certificate sizes and regeneration path is good; adding the Lean theorem statement’s dependency on the equisatisfiability lemma name in the text would help readers navigate the development.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: end-to-end Lean certificates and parametric reformulation proofs do not reduce to fitted inputs or load-bearing self-citation chains.

full rationale

LeanCSP’s central claims are systems and formalization claims: parametric equivalence/equisatisfiability/SBC soundness in Lean, a library-wide CSP-to-PB soundness theorem, and instance-level certificate checking that yields Lean (un)satisfiability theorems about the stated CSP. Combinatorial demos (e.g. schur_4_exact, R(3,3) and W(2,3) bounds) re-establish classical external facts via that pipeline; they are not quantities defined from the method’s own outputs. Experimental speedups compare the same solver with/without verified SBCs on deterministic operation counts and wall time—empirical baselines, not fitted-then-predicted parameters. Citations to PBLean and related Lean tooling are infrastructure dependencies with independent checker semantics (reflection of a once-proved checker); they do not smuggle an ansatz or uniqueness theorem that forces the paper’s results by construction. The disclosed trust boundary (Lean CSP as specification; Lean.ofReduceBool/Lean.trustCompiler) is standard TCB disclosure, not circular derivation. No self-definitional loop, fitted-input-as-prediction, or renaming of a known empirical law appears in the derivation chain.

Assumptions & free parameters 0 free parameters · 5 assumptions · 2 invented entities

The central claims rest on standard type-theoretic foundations, the Lean kernel/compiler trust model for reflection-based checking, the modeling choice that the Lean CSP is the specification, and soundness of the library’s CSP-to-PB encodings. No fitted scientific parameters. Invented entities are software abstractions, not physical posits.

assumptions (5)
  • domain assumption Lean kernel correctness plus reflection axioms Lean.ofReduceBool and Lean.trustCompiler (Lean compiler in TCB) when PBLean/bv_decide-style checkers succeed
    Section 3 explicitly places these in the trusted base for in-Lean certificate checking by reflection.
  • domain assumption The Lean CSP model is identified with the mathematical problem specification (not merely an encoding of a separate ground truth)
    Stated in Section 3; all end-to-end theorems are about isSatisfiableInt of that model.
  • domain assumption For every library constraint, satisfiability of the CSP constraint implies satisfiability of its intermediate pseudo-Boolean representation (CSP→PB soundness)
    Required to lift PBLean UNSAT on the PB model to UNSAT of the original CSP; claimed proved per constraint in Section 3.
  • standard math Standard CSP solution/assignment semantics and classical definitions of equisatisfiability and solution-set bijection equivalence
    Section 2 basic definitions following Rossi et al.; used throughout reformulation theorems.
  • domain assumption Finite integer domains and constraints drawn from the predefined library for the translation/certification path
    Section 3 restricts automatic translation and certificate pipelines to this subclass.
invented entities (2)
  • LeanCSP DynamicConstraint / dependent-type CSP encoding and π-equivalence layer independent evidence
    purpose: Represent arbitrary-arity CSPs in Lean and prove parametric equivalence/equisatisfiability/SBC lemmas
    Software formalization choice; independent evidence is the public Lean development and discharged theorems, not an external physical prediction.
  • Generic value-precedence symmetry-breaking constraint proved once for interchangeable values independent evidence
    purpose: Amortize SBC soundness across families (Schur, coloring, PHP, Ramsey, vdW)
    Reusable verified lemma (149 lines generic + glue); validated by typechecked proofs and measured solver speedups.

how reviews work

0 comments
Cite this review

Pith. "Pith review of LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean." pith.science (2026). https://pith.science/paper/M344AYBG

@misc{pith2026260728459,
  author       = {Pith},
  title        = {Pith review of: LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/M344AYBG}},
  note         = {Machine review of arXiv:2607.28459}
}
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2607.28459 by the authors.

Figure 1
Figure 1. Overview of LeanCSP. A CSP P can be formulated in Lean, and a reformulation (an equivalence or equisatisfiability theorem) that yields another CSP P ′ can be proven correct at the parametric level. At the instance level, a CSP is translated to an external solver format; the solver’s SAT or UNSAT certificate is checked back in Lean (by decide or PBLean, respectively), establishing an (un)satisfiability theorem. The e… view at source ↗
Figure 2
Figure 2. Proof length (proof steps, log scale) versus instance size for the pseudo-Boolean (VeriPB) [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

48 extracted references · 13 canonical work pages

  1. [1]

    Abdulaziz and F

    M. Abdulaziz and F. Kurz. Formally Verified SAT-Based AI Planning . Proceedings of the AAAI Conference on Artificial Intelligence, 37 0 (12): 0 14665--14673, June 2023. ISSN 2374-3468. doi:10.1609/aaai.v37i12.26714

    work page doi:10.1609/aaai.v37i12.26714 2023

  2. [2]

    Alekhnovich

    M. Alekhnovich. Mutilated chessboard problem is exponentially hard for resolution. Theoretical Computer Science, 310 0 (1-3): 0 513--525, Jan. 2004. ISSN 03043975. doi:10.1016/S0304-3975(03)00395-5

    work page doi:10.1016/s0304-3975(03)00395-5 2004

  3. [3]

    Barrett, A

    C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard : Version 2.0. Technical report, Department of Computer Science, The University of Iowa, 2010

    2010

  4. [4]

    Barrett, L

    C. Barrett, L. de Moura, and P. Fontaine. Proofs in Satisfiability Modulo Theories . In All about Proofs , Proofs for All , volume 55 of Mathematical Logic and Foundations , pages 23--44. College Publications, London, UK, Jan. 2015. ISBN 978-1-84890-166-7

    2015

  5. [5]

    Biere, T

    A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, and F. Pollitt. CaDiCaL 2.0. In A. Gurfinkel and V. Ganesh, editors, Computer Aided Verification , volume 14681, pages 133--152. Springer Nature Switzerland, Cham, 2024. ISBN 978-3-031-65626-2 978-3-031-65627-9. doi:10.1007/978-3-031-65627-9_7

    doi:10.1007/978-3-031-65627-9_7 2024

  6. [6]

    Bogaerts, S

    B. Bogaerts, S. Gocht, C. McCreesh, and J. Nordstr \"o m. Certified Dominance and Symmetry Breaking for Combinatorial Optimisation . Journal of Artificial Intelligence Research, 77: 0 1539--1589, Aug. 2023. ISSN 1076-9757. doi:10.1613/jair.1.14296

    doi:10.1613/jair.1.14296 2023

  7. [7]

    B \"o ving, S

    H. B \"o ving, S. Bhat, L. Cicolini, A. Keizer, L. Frenot, A. Mohamed, L. Stefanesco, H. Khan, J. Clune, C. Barrett, and T. Grosser. Interactive Bitvector Reasoning using Verified Bit-Blasting . Proceedings of the ACM on Programming Languages, 9 0 (OOPSLA2): 0 3259--3285, Oct. 2025. ISSN 2475-1421. doi:10.1145/3763167

    doi:10.1145/3763167 2025

  8. [8]

    R. E. Bryant, A. Biere, and M. J. H. Heule. Clausal Proofs for Pseudo-Boolean Reasoning . In D. Fisman and G. Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems , volume 13243, pages 443--461. Springer International Publishing, Cham, 2022. ISBN 978-3-030-99523-2 978-3-030-99524-9. doi:10.1007/978-3-030-99524-9_25

    work page doi:10.1007/978-3-030-99524-9_25 2022

Show all 48 references
  1. [9]

    Carlier, C

    M. Carlier, C. Dubois, and A. Gotlieb. A Certified Constraint Solver over Finite Domains . In D. Giannakopoulou and D. M \'e ry, editors, FM 2012: Formal Methods , pages 116--131, Berlin, Heidelberg, 2012. Springer. ISBN 978-3-642-32759-9. doi:10.1007/978-3-642-32759-9_12

    2012 doi

  2. [10]

    Carneiro

    M. Carneiro. Lean4Lean : Verifying a Typechecker for Lean , in Lean . arXiv:2403.14064, Sept. 2025

    2025 arXiv

  3. [11]

    G. Chu, P. J. Stuckey, A. Schutt, T. Ehlers, G. Gange, and K. Francis. Chuffed, a lazy clause generation solver. https://github.com/chuffed/chuffed, 2023

    2023

  4. [12]

    C. R. Codel, J. Avigad, and M. J. H. Heule. Verified Encodings for SAT Solvers . In 2023 Formal Methods in Computer-Aided Design ( FMCAD ) , pages 141--151, Oct. 2023. doi:10.34727/2023/isbn.978-3-85448-060-0_22

    2023 doi

  5. [13]

    Cohen, P

    D. Cohen, P. Jeavons, C. Jefferson, K. E. Petrie, and B. M. Smith. Symmetry Definitions for Constraint Satisfaction Problems . In D. Hutchison, T. Kanade, J. Kittler, J. M. Kleinberg, F. Mattern, J. C. Mitchell, M. Naor, O. Nierstrasz, C. Pandu Rangan, B. Steffen, M. Sudan, D....

    2005

  6. [14]

    W. Cook, C. Coullard, and Gy . Tur \'a n. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18 0 (1): 0 25--38, Sept. 1987. ISSN 0166218X. doi:10.1016/0166-218X(87)90039-4

    1987 doi

  7. [15]

    Cruz-Filipe , M

    L. Cruz-Filipe , M. J. H. Heule, W. A. Hunt, M. Kaufmann, and P. Schneider-Kamp . Efficient Certified RAT Verification . In L. de Moura , editor, Automated Deduction -- CADE 26 , pages 220--236, Cham, 2017. Springer International Publishing. ISBN 978-3-319-63046-5. doi:10.1007...

    2017 doi

  8. [16]

    Cruz-Filipe , J

    L. Cruz-Filipe , J. Marques-Silva , and P. Schneider-Kamp . Formally Verifying the Solution to the Boolean Pythagorean Triples Problem . Journal of Automated Reasoning, 63 0 (3): 0 695--722, Oct. 2019. ISSN 1573-0670. doi:10.1007/s10817-018-9490-4

    2019 doi

  9. [17]

    de Moura and S

    L. de Moura and S. Ullrich. The Lean 4 Theorem Prover and Programming Language . In A. Platzer and G. Sutcliffe, editors, Automated Deduction -- CADE 28 , pages 625--635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5. doi:10.1007/978-3-030-79876-5_37

    2021 doi

  10. [18]

    R. Dechter. Constraint Processing . Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, Apr. 2003. ISBN 978-1-55860-890-0

    2003

  11. [19]

    C. Dubois. Formally Verified Transformation of Non-binary Constraints into Binary Constraints . arXiv:2009.00583, Sept. 2020

    2009 arXiv

  12. [20]

    Elffers and J

    J. Elffers and J. Nordstr \"o m. Divide and conquer: Towards faster Pseudo-Boolean solving. In J. Lang, editor, Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018, pages 1291--1299. ijcai.org, 2018. doi:10.24963/ijcai.2018/180

    2018 doi

  13. [21]

    Flippo, K

    M. Flippo, K. Sidorov, I. Marijnissen, J. Smits, and E. Demirovi \'c . A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers . In P. Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming ( CP 2024) , volume 30...

    2024 doi

  14. [22]

    I. P. Gent, K. E. Petrie, and J.-F. Puget. Symmetry in Constraint Programming . In F. Rossi, P. van Beek, and T. Walsh, editors, Handbook of Constraint Programming , volume 2 of Foundations of Artificial Intelligence , pages 329--376. Elsevier, 2006. doi:10.1016/S1574-6526(06)80014-3

    2006 doi

  15. [23]

    Gocht and J

    S. Gocht and J. Nordstr \"o m. Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs . Proceedings of the AAAI Conference on Artificial Intelligence, 35 0 (5): 0 3768--3777, May 2021. ISSN 2374-3468. doi:10.1609/aaai.v35i5.16494

    2021 doi

  16. [24]

    Gocht, C

    S. Gocht, C. McCreesh, and J. Nordstr \"o m. An Auditable Constraint Programming Solver . In C. Solnon, editor, 28th International Conference on Principles and Practice of Constraint Programming ( CP 2022) , volume 235 of Leibniz International Proceedings in Informatics ( LIPI...

    2022 doi

  17. [25]

    Gocht, C

    S. Gocht, C. McCreesh, M. O. Myreen, J. Nordstr \"o m, A. Oertel, and Y. K. Tan. End-to- End Verification for Subgraph Solving . Proceedings of the AAAI Conference on Artificial Intelligence, 38 0 (8): 0 8038--8047, Mar. 2024. ISSN 2374-3468, 2159-5399. doi:10.1609/aaai.v38i8.28642

    2024 doi

  18. [26]

    W. T. Gowers, B. Green, F. Manners, and T. Tao. On a conjecture of Marton . Annals of Mathematics, 201 0 (2): 0 515--549, Mar. 2025. ISSN 0003-486X, 1939-8980. doi:10.4007/annals.2025.201.2.5

    2025 doi

  19. [27]

    A. Haken. The intractability of resolution. Theoretical Computer Science, 39: 0 297--308, 1985. ISSN 03043975. doi:10.1016/0304-3975(85)90144-6

    1985 doi

  20. [28]

    M. J. Heule, W. A. Hunt, and N. Wetzler. Trimming while checking clausal proofs. In 2013 Formal Methods in Computer-Aided Design , pages 181--188, Oct. 2013. doi:10.1109/FMCAD.2013.6679408

    2013

  21. [29]

    M. J. H. Heule. Schur number five. In Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence and Thirtieth Innovative Applications of Artificial Intelligence Conference and Eighth AAAI Symposium on Educational Advances in Artificial Intelligence , AAAI '18...

    2018 doi

  22. [30]

    M. N. Mansur, M. Christakis, V. W \"u stholz, and F. Zhang. Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineeri...

    2020

  23. [31]

    Mohamed, T

    A. Mohamed, T. Mascarenhas, H. Khan, H. Barbosa, A. Reynolds, Y. Qian, C. Tinelli, and C. W. Barrett. Lean- SMT : An SMT tactic for discharging proof goals in Lean . In Computer Aided Verification -- 37th International Conference, CAV 2025, Proceedings, Part III, volume 15933 ...

    2025 doi

  24. [32]

    Nethercote, P

    N. Nethercote, P. J. Stuckey, R. Becket, S. Brand, G. J. Duck, and G. Tack. MiniZinc : Towards a Standard CP Modelling Language . In C. Bessi \`e re, editor, Principles and Practice of Constraint Programming -- CP 2007 , pages 529--543, Berlin, Heidelberg, 2007. Springer. ISBN...

    2007 doi

  25. [33]

    Nipkow, L

    T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/ HOL : A Proof Assistant for Higher-Order Logic . Number 2283 in Lecture Notes in Computer Science. Springer, Berlin New York, 2002. ISBN 978-3-540-45949-1

    2002

  26. [34]

    Rossi, P

    F. Rossi, P. van Beek , and T. Walsh, editors. Handbook of Constraint Programming. Foundations of Artificial Intelligence. Elsevier, 2006. ISBN 978-0-444-52726-4

    2006

  27. [35]

    Roussel and V

    O. Roussel and V. Manquinho. Input/ Output Format and Solver Requirements for the Competitions of Pseudo-Boolean Solvers . https://www.cril.univ-artois.fr/PB16/format.pdf, 2016

    2016

  28. [36]

    Schulte, G

    C. Schulte, G. Tack, and M. Z. Lagerkvist. Modeling and Programming with Gecode . https://github.com/Gecode/gecode, 2019. Corresponds to Gecode 6.2.0

    2019

  29. [37]

    A. Stump. Verified Functional Programming in Agda . Number 9 in ACM Books. Association for Computing Machinery, New York, NY, 2016. ISBN 978-1-970001-27-3 978-1-970001-26-6 978-1-970001-25-9. doi:10.1145/2841316

    2016 doi

  30. [38]

    Subercaseaux, W

    B. Subercaseaux, W. Nawrocki, J. Gallicchio, C. Codel, M. Carneiro, and M. J. H. Heule. Formal Verification of the Empty Hexagon Number . LIPIcs, Volume 309, ITP 2024, 309: 0 35:1--35:19, 2024. ISSN 1868-8969. doi:10.4230/LIPICS.ITP.2024.35

    2024 doi

  31. [39]

    S. Szeider. Leanback: MCP server for Lean 4 theorem proving --- check, prove, goals, eval, search. https://pypi.org/project/leanback/, 2026 a

    2026

  32. [40]

    S. Szeider. PBLean : Pseudo-Boolean Proof Certificates for Lean 4. In 17th International Workshop on Pragmatics of SAT ( PoS 2026), a workshop of SAT 2026 and FLoC 2026 , Lisbon, Portugal, July 2026 b . To appear. Preprint available at https://arxiv.org/abs/2602.08692

    2026

  33. [41]

    Colibrics: A Formally Verified Constraint Programming Engine

    The Colibri Team . Colibrics: A Formally Verified Constraint Programming Engine . https://colibri.frama-c.com/, 2019

    2019

  34. [42]

    The Lean Language Reference

    The Lean Developers . The Lean Language Reference . https://lean-lang.org/doc/reference/latest/, 2026

    2026

  35. [43]

    The lean mathematical library

    The mathlib Community . The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , CPP 2020, pages 367--381, New York, NY, USA, Jan. 2020. Association for Computing Machinery. ISBN 978-1-4503-7097-4. doi:10....

    2020

  36. [44]

    The Rocq Prover

    The Rocq Development Team . The Rocq Prover . Zenodo, Apr. 2025

    2025

  37. [45]

    E. Tsang. Foundations of Constraint Satisfaction. Academic Press, London San Diego, 1993. ISBN 978-0-12-701610-8

    1993

  38. [46]

    van Doorn , P

    F. van Doorn , P. Massot, and O. Nash. Formalising the h- Principle and Sphere Eversion . In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs , CPP 2023, pages 121--134, New York, NY, USA, Jan. 2023. Association for Computing Machin...

    2023

  39. [47]

    Vanroose, I

    W. Vanroose, I. Bleukx, J. Devriendt, D. Tsouros, H. Verhaeghe, and T. Guns. Mutational Fuzz Testing for Constraint Modeling Systems . In P. Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming ( CP 2024) , volume 307 of Leibniz Inte...

    2024 doi

  40. [48]

    Wetzler, M

    N. Wetzler, M. J. H. Heule, and W. A. Hunt. DRAT-trim : Efficient Checking and Trimming Using Expressive Clausal Proofs . In C. Sinz and U. Egly, editors, Theory and Applications of Satisfiability Testing -- SAT 2014 , pages 422--429, Cham, 2014. Springer International Publish...

    2014 doi

Pith tools

Reviewed July 31, 2026 · model on record in the stance chip above.