A total-search core, checked in Lean
A machine-checked Lean 4 formalization of the finite explicit-sampler core behind the Heavy Avoid problem from FOCS 2024.
The work defines the induced distribution of a finite sampler, formalizes heavy sets, and proves that a light output exists in the total-search regime.
It also implements a deterministic exhaustive solver and proves that its output satisfies the specification using exact rational arithmetic.
The scope is deliberately narrow: it proves the finite existence and search core, not a polynomial-time solver for the general problem.
where the effort went
the numbers
built with
delivery record
I wanted to separate the exact combinatorial statement that can be verified today from the broader complexity claim that remains research work.
Finite sampler and induced-distribution definitions
Heavy-set cardinality bounds over exact rationals
Machine-checked proof that a light output exists
Deterministic exhaustive solver with a proved specification
Source-audited build with no sorry, admit, custom axiom, or unsafe escape
The constraints mattered as much as the finished interface.
after shipping
Formalization is most useful when it narrows a claim to exactly what the proof establishes.
A proved exponential solver can still be valuable as a specification and a base for future refinements.