Quantum computers
Count how often each machine looks at its input. For a yes-or-no question with an answer for every input, an ordinary computer needs at most a fixed multiple of the quantum count to the fourth power, and OpenAI showed that no smaller power works. Lean checks that whole theorem here.
Limits: The count is of looks at the input, which is a different measure from running time. The labels that compare each Lean statement with the paper are AI-written, and no expert has reviewed them yet.
The result is OpenAI’s, released in October 2026. It matches an upper bound proved in 2020.
Lean is a program that checks mathematical proofs.
