{"id":"lean/anthropics__formal-math__eth","url":"https://github.com/anthropics/formal-math/tree/main/eth","repo":"https://github.com/anthropics/formal-math","score":0,"title":"A 2 o(*n*) Time Algorithm for 3-SAT","source":"lean","authors":["anthropics"],"reviews":0,"summary":"A deterministic algorithm solves 3-SAT on *n* variables in time 2 o(*n*) , which refutes the Exponential Time Hypothesis (ETH). The algorithm in fact solves the harder problem #3-SAT, counting the satisfying assignments, in time 2 O(*n* log log *n* / √log *n*) .","category":"research","comments":0,"disputed":false,"mentions":0,"discussed":0,"published":"2026-08-06","reactions":{},"formalized":true}