OpenAI couples natural language and Lean to disprove complexity conjecture

OpenAI has published research pairing natural-language reasoning with machine-checked Lean code to disprove the Eigenvalue-Trace Heuristic conjecture in complexity theory.

The effort, disclosed in an outline of the laboratory's scientific collaborations with academic communities, demonstrates an end-to-end mathematical workflow. Rather than relying solely on informal prose, the model generated both a human-readable mathematical argument and formal code verifiable by the Lean interactive theorem prover.

The Eigenvalue-Trace Heuristic conjecture originated within computational complexity and spectral analysis. For years, the conjecture resisted resolution, with researchers evaluating whether specific matrix trace bounds held universally across structured cases. OpenAI's frontier reasoning model identified an explicit counterexample. Crucially, the system formalised its steps into Lean definitions and lemmas, allowing the theorem prover's kernel to verify the counterexample without human trust assumptions.

Formal theorem proving has historically required laborious manual encoding by specialists. While automated reasoning engines operate over constrained domains, mapping natural-language mathematical intuition into dependent type theory remains an active bottleneck. By supplying natural-language exposition alongside formal Lean scripts, the system offers human mathematicians an interpretable narrative of why the conjecture fails, paired with deterministic mathematical certainty.

OpenAI framed the result as part of a wider programme to evaluate model utility within active scientific discovery. The lab highlighted that academic partnerships remain essential for validating whether such proofs advance domain knowledge or resolve narrow technical edge cases. Unlike traditional applications where language models can generate specious algebraic manipulations, coupling reasoning chains to formal verification kernels guarantees correctness at runtime.

The disproof arrives as mathematical institutions increasingly adopt formal methods to audit complex modern proofs. Projects such as Lean's Mathlib have grown rapidly, yet the manual formalisation of cutting-edge literature continues to lag behind publication rates.

If frontier models can reliably generate machine-checked refutations to open conjectures, will theoretical computer science shift toward automated refereeing systems that demand Lean verification alongside initial preprint submissions?