Claim 4.2 — MinWork is strongly truthful

Proved

AlgMechDesign.MinWork.minwork_strongly_truthful

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

mechanism-designp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1schedulingtruthfulness

Let $n \ge 2$ and $k \ge 0$ , and let $x(\cdot)$ be any MinWork allocation rule, with the MinWork payments $p^i(d) = \sum_{j \in x^i(d)} \min_{i' \neq i} d^{i'}_j$ . Then the mechanism $(x, p)$ is strongly truthful on positive types:

for every positive declaration profile $d^{-i}$ of the others, every positive true type $t^i$ and every positive misreport $d^i$ ,

u^i\big(t^i \mid (d^i, d^{-i})\big) \le u^i\big(t^i \mid (t^i, d^{-i})\big), \qquad u^i(t^i \mid d) = p^i(d) - \sum_{j \in x^i(d)} t^i_j ;

for every positive $t^i$ and every positive $d^i \neq t^i$ there is a positive $d^{-i}$ for which this inequality is strict.

That is, truth-telling is the only dominant strategy of each agent, for any number of tasks and any tie-breaking rule.

Formalization Note The paper writes its proof of the strict part for one task and two agents ("The argument for $k > 1$ is similar"); the statement here is for every $n \ge 2$ and every $k$ . The printed proof also swaps the two utilities in the case $d^i > t^i$ (see the mission's description).

Preamble

import Mathlib
import Definitions.Def_AlgMechDesign_MinWork_Model
import Definitions.Def_AlgMechDesign_MinWork_Mechanism

Formal statement

namespace AlgMechDesign.MinWork

/-- Claim 4.2: for `n ≥ 2` agents, any number `k` of tasks and every tie-breaking rule, the
MinWork mechanism is strongly truthful on positive types. -/
theorem minwork_strongly_truthful {n k : ℕ} (hn : 2 ≤ n)
    (alloc : (Fin n → Fin k → ℝ) → (Fin k → Fin n)) (hmin : IsMinWorkAlloc alloc) :
    IsStronglyTruthful alloc (minWorkPay hn alloc) := by sorry

end AlgMechDesign.MinWork

Source

Nisan, Ronen, Algorithmic Mechanism Design, Games Econ. Behav. 35, 2001, p. 176, Claim 4.2 (proof p. 177)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph