A work-in-progress formalization of a paper by Brakensiek et al. which used a SAT encoding to prove that Keller's conjecture is false in dimension 7.

Compared to most data types, collections have large interfaces. There might be a dozen "basic" operations on a collection, and then users expect dozens more convenience functions to be available.

Shared interface specifications help implementers manage this overwhelming breadth of functionality. They also can allow for code deduplication via generic implementations of those convenience functions.

Lean core has a growing selection of collection datatypes, but no typeclasses to generalize across them. This library attempts to add these typeclasses.

The more interesting goal is to generalize correctness of collection manipulations across these interfaces. Proofs about collection code are painful. Tactics frequently expose implementation details which complicate otherwise-straightforward proofs.

The library somewhat works for generalizing code, but currently mostly fails at generalizing correctness.

Boolean satisfiability (SAT) has proven to be a remarkably useful interface for solving concrete instances of combinatorial and NP-complete problems.

Given a combinatorial problem, we can usually encode it straightforwardly into the language of SAT. From there, we can take advantage of decades of research on efficient SAT solving techniques to get a practical solver for our original combinatorial problem.

Q: How do you ensure the encoding is correct? If your original problem P is encoded into the SAT problem Q, and Q has no solution, does that mean P has no solution?

A: Formal verification. Trestle is a Lean 4 library which allows users to write -- and verify -- encodings from arbitrary problem domains to SAT.