AI Proof WatchKeep up with AI contributions

Kemeny Rank Aggregation is NP-Hard for Three Voters

Dominik Peters

KEMENY SCORE is NP-complete for exactly three unweighted complete rankings. Peters reduces from SIMPLE MAX CUT with long even edges to a unit-margin majority tournament realizable by three voters.

Sources for this record

What was already known

Hardness was known for four even voters and seven odd voters; one or two voters were tractable. The three-voter case had been open for 25 years.

AI involvement AI-led

Peters credits GPT-5.6 Sol Ultra with finding the three-voter reduction. Peters selected the target and prior papers and simplified, explained and formalized the final argument with model help.

GPT is specifically credited with the three-voter reduction, while Peters guided the task and materially simplified the final proof. The two listings are duplicates of one AI-led contribution.

Importance Major

Closes the three-voter complexity question for Kemeny rank aggregation.

Limitations

The Lean project reports a certified reduction and successful build. Madarasi independently proved the same conclusion but did not check Peters’s reduction; his later complexity results are separate.

Technical verification Formal (Lean 4 with the HardnessReductions certified-reduction library)

Peters's companion Lean project contains a certified version of the three-voter reduction and reports a successful CI build at its August 7 revision. The machine check is source-reported. Madarasi's separate proof confirms the theorem but does not verify the original reduction.

Formal checking

Formal reduction equivalence and program adequacy proof, certified SAT-to-Kemeny composition, successful CI build at commit ca9478b0b30be430f58e9a9f200fd5d999796156

Checker
Lean 4 kernel in the repository's Lean Action CI
Scope
Correctness and polynomial-time certificate for Peters's three-voter KEMENY SCORE reduction
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Full

Peters's §§1–5 explain the final gadget, majority realization and correctness argument, and explicitly identify his simplifying mathematical input. Madarasi explains an independent proof of the same theorem, which is not treated as an explanation of Peters's mechanism.

Correction and publication history