TCS researcher: release includes a claimed, Lean-formalized proof of the Unique Games Conjecture he had worked on

Posted 23:22 UTC, quoting OpenAI: "This includes a claimed proof and Lean formalization of the Unique Games Conjecture, which I have been personally working on for the last year and a half." ~91k views. Bebel's bio: theoretical computer scientist, formerly USC.

Other UGC reactions: Chris Peikert (Michigan) at 23:43 UTC: "Unique Games Conjecture, proved. L=RL, proved. And that’s just the first two CS results…" (https://x.com/ChrisPeikert/status/2107617657415782731, ~12k views). Mahdi Ch. (@mahdi_tcs_, CS professor at Michigan per his bio) at 00:17 UTC: "Unique Games Theorem, shorter than a typical FOCS/STOC paper" (https://x.com/mahdi_tcs_/status/2107626269969895838, ~3.4k). No expert had reported checking the proof by 05:20 UTC; the claimed Lean formalization was the main basis for confidence.

This includes a claimed proof and Lean formalization of the Unique Games Conjecture, which I have been personally working on for the last year and a half.

Quoting @OpenAI: We’re releasing a broad range of new mathematical results produced by an internal frontier model.

We’ve been consulting with the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study, and we have drawn on their advice and

likes 1368 · replies 21 (at fetch time)

Archived 2026-10-07 via syndication.