Anthropic 发布 Claude 发现的 3-SAT 2^o(n) 时间算法及 Lean 4 形式化

Anthropic 在 GitHub 发布论文，提出一个确定性算法在 2^o(n) 时间内求解 n 个变量的 3-SAT，并称这推翻了指数时间假设（ETH）；该算法实际求解更难的 #3-SAT 计数问题，时间为 2^O(n log log n / √log n)。