The Ramachandra-Natarajan Pairwise Independent Correlation Gap Conjecture
Ramachandra and Natarajan conjectured a bound on the pairwise independent correlation gap in their 2025 Operations Research Letters paper. An explicit counterexample refutes it.
- Result
- Disproved
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Optimization
- Posed by
- Arjun Ramachandra, Karthik Natarajan
- Year posed
- 2025
- Years open
- 1y
- Solved
- 2026-06-18
- Model
- GPT-5.5 Pro
- Vendor
- OpenAI
- Collaborators
- Arjun Ramachandra, Karthik Natarajan
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 7 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
The abstract credits the counterexample to GPT-5.5 Pro in its first sentence. The authors add that earlier attempts with free tiers of ChatGPT and Claude made no progress, which is a useful data point on where the capability threshold sat. They are refuting their own conjecture.
Verification
The refutation is an explicit counterexample, so it is a finite check. Short arXiv note, not peer-reviewed.
A Lean 4 / Mathlib formalization of the counterexample was contributed in August 2026 by its author, produced with Codex. Curator source audit: all 579 lines read, with no sorry, admit, native_decide, unsafe declaration, user-declared axiom, implemented_by or partial def anywhere; finite checks go through kernel decide and rational identities through norm_num, and Mathlib is pinned to an exact revision on toolchain v4.33.0-rc2. The curator has not compiled it, and it is the work of the same person who reported the result, so it is not third-party corroboration.
What the formalization does and does not settle is worth stating exactly. Its final theorem is a seven-part conjunction certifying the witness and its bounds: the three-atom distribution attains the target marginals with expected coverage 4, no distribution exceeds 4, the product distribution is pairwise feasible, every pairwise-feasible distribution is bounded by , and . Both bounds are universally quantified rather than spot-checked. What the file never states is the Ramachandra-Natarajan conjecture itself, so the step from this instance to the conjecture being refuted stays informal and rests on the conjectured bound really being . That is the difference between a kernel-checked artifact and an audited claim, and why this sits on the unaudited Lean rung.
An independent auditor is wanted for this entry.
The counterexample now has a public Lean 4 / Mathlib formalization, contributed by its author and produced with Codex: https://github.com/Olangu/pairwise-correlation-gap-lean
I have read the source and found no sorry, admit, native_decide, unsafe declaration or user-declared axiom, and the dependencies are pinned, so the build should be reproducible. Two things I have not done, and either would move this entry up the verification ladder:
1. Compile it. The repository claims a clean build whose final theorem depends only on propext, Classical.choice and Quot.sound. Anyone who runs it and confirms the axiom list has reproduced the artifact.
2. Audit the correspondence. This is the more valuable one. The Lean file certifies the witness and its two bounds; it never states the Ramachandra-Natarajan conjecture, so nothing formal yet connects 640/479 > 4/3 to the conjecture being false. Someone who knows the correlation-gap literature could check that the formal model really is the paper's instance and that the conjectured bound is 4/3.
If you take either on, say so here and the entry will record what you found.