# Quasipolynomial algorithms for mean-payoff, stochastic and parity games

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Deterministic quasipolynomial-time mean-payoff games](../../preprints/Deterministic-quasipolynomial-time-mean-payoff-games-September-25-2026/paper.pdf)
- [Randomized quasipolynomial-time mean-payoff games](../../preprints/Randomized-quasipolynomial-time-mean-payoff-games-September-25-2026/paper.pdf)

## Scope

The formalization checks that a specified two-step execution of Truffet's elimination procedure terminates with a feasible but nonoptimal output. It is a finite counterexample to that proposed optimization step.

The formalized result gives one randomized algorithm for the complete zero-threshold winning set of every finite mean-payoff game with signed binary weights. It succeeds with probability at least $7/8$ and runs in quasipolynomial bit time on every random tape. Self-loops, parallel edges, and history-dependent strategies are allowed, and winning means a nonnegative liminf average payoff.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Finite counterexample to Truffet's optimization procedure | [TruffetCounterexample.lean](../ComparatorChallenges/TruffetCounterexample.lean) |
| Randomized quasipolynomial mean-payoff algorithm | [RandomizedMeanPayoff.lean](../ComparatorChallenges/RandomizedMeanPayoff.lean) |