General-Valued Constraint Satisfaction Problems

This is a playground for experiments preceding our contribution to the Lean 4 version of Mathlib.

Permalink to the definition of VCSP in Mathlib

Our long-term goal is to formalize the dichotomy for fixed-template finite-valued constraint satisfaction problems [Thapper, Živný, Kolmogorov] while exploring potential generalizations (infinite domains, partially ordered codomains, and more).


Main results (please see the definitions in ValuedCSP.lean first)

Farkas-like theorems (can be use independently of the VCSP)

Mathlib contributions that stem from this project

Pull requests (these PRs are compatible with each other)

Proposals for Linear Programming (these PRs are incompatible with each other)