Anthropic posts a paper claiming a subexponential-time algorithm for 3-SAT, with a Lean 4 formalization
If correct, the result would refute the Exponential Time Hypothesis; the proof's axioms are documented in the repository, and independent expert review has not been published.