This condition succeeds when at least one of A, B, or C is true.
SPECIAL INVESTIGATION 001 / LOGIC AND EVIDENCE
The 3-SAT ChallengeWhen impossible meets evidence.
Can you make every logical condition true at once? Investigate a tiny 3-SAT puzzle, then examine why a remarkable new scientific claim needs more than a persuasive headline.
PART 01 / LEARN THE RULES
Three switches. Four conditions.
Imagine three switches named A, B, and C. Each is either TRUE (on) or FALSE (off). A condition is satisfied when at least one of its three statements is true. Your mission is to find a single switch setting that makes all four conditions true.
The symbol ¬A means A must be false for that particular statement to be true.
Different conditions are combined with AND: all of them must succeed.
In 3-SAT, each condition is a clause containing exactly three literals (variables or their negations). The clauses are connected by AND.
CLAUSE 01A ∨ B ∨ C
CLAUSE 02¬A ∨ B ∨ ¬C
CLAUSE 03A ∨ ¬B ∨ C
CLAUSE 04¬A ∨ ¬B ∨ C
THE COMPLETE PUZZLE
(A ∨ B ∨ C) ∧ (¬A ∨ B ∨ ¬C) ∧ (A ∨ ¬B ∨ C) ∧ (¬A ∨ ¬B ∨ C)
YOUR TURN_
Before revealing the answers, try setting A = TRUE, B = FALSE, C = FALSE. Does every clause succeed? Then try setting all three switches to FALSE. What changes?
Reveal the first worked answer
With A = TRUE, B = FALSE, C = FALSE, clause 01 succeeds because A is true. Clause 02 succeeds because ¬C is true. Clauses 03 and 04 also succeed (A in clause 03, ¬B in clause 04).
All four clauses are true. This one assignment is enough to prove that the example formula is satisfiable.
What happens when all three are FALSE?
Clause 01 becomes FALSE ∨ FALSE ∨ FALSE, which is false. The other three clauses are true, but that is not enough: all four are connected by AND.
This assignment does not satisfy the formula. That does not mean the formula is unsatisfiable, because another assignment already works.
PART 02 / CHECK THE EVIDENCE
Eight candidates. Not eight guesses.
With three Boolean variables, there are 2 × 2 × 2 = 8 assignments. To establish that the formula is satisfiable, you need just one working assignment. To establish that it is unsatisfiable by exhaustive checking, you would have to rule out every possible assignment.
Reveal the complete truth table and verify the puzzle
Each column labelled C1 through C4 reports whether that clause is true. “SAT” means all four are true in the same row. This table is exhaustive for these three variables.
| TRY | A | B | C | C1 | C2 | C3 | C4 | ALL? |
|---|---|---|---|---|---|---|---|---|
| 01 | F | F | F | FALSE | TRUE | TRUE | TRUE | NO |
| 02 | F | F | T | TRUE | TRUE | TRUE | TRUE | SAT |
| 03 | F | T | F | TRUE | TRUE | FALSE | TRUE | NO |
| 04 | F | T | T | TRUE | TRUE | TRUE | TRUE | SAT |
| 05 | T | F | F | TRUE | TRUE | TRUE | TRUE | SAT |
| 06 | T | F | T | TRUE | FALSE | TRUE | TRUE | NO |
| 07 | T | T | F | TRUE | TRUE | TRUE | FALSE | NO |
| 08 | T | T | T | TRUE | TRUE | TRUE | TRUE | SAT |
Cross-check: four rows satisfy every clause: (F, F, T), (F, T, T), (T, F, F), and (T, T, T). Four rows fail at least one clause.
Why not test every assignment in a large problem?
For n Boolean variables there are 2n possible assignments. A brute-force search may inspect many of them, but a smarter algorithm can sometimes exploit the structure of clauses and avoid examining every assignment individually.
1,048,576 possible settings. Many are manageable with modern algorithms and useful structure, but the number of possible settings grows rapidly.
1,125,899,906,842,624 possible settings. This is the size of the brute-force search space—not a claim that every solver examines every setting.
PART 03 / REAL-WORLD RESEARCH
What exactly did OpenAI announce?
On 26 October 2026, OpenAI published a research announcement stating that an internal AI system had produced a claimed refutation of the Exponential Time Hypothesis (ETH), a long-standing conjecture about the worst-case complexity of problems including 3-SAT. OpenAI released a manuscript and Lean formalization, and described an independent group of complexity researchers convening to examine and explain the result.
ETH informally says there is no subexponential-time algorithm for 3-SAT, as a function of the number of variables, in the standard worst-case setting. A correct subexponential-time algorithm would overturn that conjecture. The announced result concerns a theoretical asymptotic bound, not a practical benchmark for this page's little puzzle.
A new subexponential theoretical algorithm for counting solutions of fixed-width Boolean formulas, with consequences for ETH and 3-SAT if the result withstands scrutiny.
It does not prove P = NP, supply a universally practical solver, or mean that real-world cryptography or every hard optimization task is suddenly broken.
Why is Lean verification important, but not the final word?
A proof assistant checks whether a formally expressed argument follows from its specified definitions and rules. Expert review still needs to check that those definitions express the intended theorem, that the mathematical scope is understood, and that the result connects correctly to the claims being made.
Investigate the strength of the scientific evidence
- Claim: What precise algorithmic guarantee does the manuscript state?
- Formal statement: What exactly was checked in Lean? Is its bound or formulation identical to the strongest claim?
- Independent review: Can experts reconstruct and explain the argument, or identify an incorrect assumption?
- Consequences: Which established conditional results really depend on ETH in the relevant form?
- Practical relevance: Can the technique become an implementable speedup on useful instances? This is a separate question from asymptotic theory.
Editorial note: this is an independent learning explanation, not an original validation of OpenAI’s proof. Its scientific status may change as experts publish further assessments.
PART 04 / TRANSFER THE SKILL
The problem-management connection.
An investigator's job is not to defend the first explanation. It is to make assumptions explicit, compare alternatives, test what could prove them wrong, and communicate the confidence justified by the evidence.
Here: find a setting that satisfies every clause—or explain a reliable method for larger instances.
One successful assignment settles satisfiability; one failing assignment does not establish impossibility.
A truth table proves the toy result; a machine-checked theorem and independent scrutiny serve different roles in research.
A powerful question to take away
“What evidence would make my preferred explanation less likely?” That question can improve an incident investigation, a root-cause analysis, an engineering decision and the evaluation of an extraordinary scientific announcement.
SOURCE NOTES_
Read the original research context.
The toy clauses and solutions in this lesson are original educational examples, independent of the algorithm claimed in the research.
- OpenAI — Working with academic communities to build scientific understanding (26 October 2026): the announcement, research context and independent review plan.
- OpenAI’s public mathematical research repository: research materials, manuscripts and formal proof artifacts linked from the announcement. Consult the ETH-related files and scope notes for the actual formal statements.
Independent educational feature by problem.me. Not affiliated with OpenAI and not an assertion that the ETH claim has been independently validated.