Rooke claims 69 Lean-checked SAT theorems and 22.92x speedup over CaDiCaL, P vs NP still open
TinfoilTricorn · x · 2026-10-30
The post relays a review of Rooke's public statements: he reports 69 Lean-checked SAT theorems, exact counting on structured problems, and a restricted algorithm with complexity O(3^b·poly(L)), plus a 22.92x performance advantage over CaDiCaL 3.0 on a benchmark. The reviewer stresses these are self-reported findings, not independently established.
Importantly, Rooke explicitly acknowledges that P versus NP remains open: an infinite family can be mathematically interesting without establishing an advantage over general-purpose SAT solvers or resolving worst-case complexity.
More from Research
- Stanford releases RT-J, a System 1 model predicting structured data in one forward pass — jure · 2026-10-30
- Generalist AI ships GEN-1.5 and challenges the community to SLAM its wrist-cam data — E0M · 2026-10-30
- Signal65 Launches PINNACLE Coding Agent Benchmark: One Model Aces 97% of Samples, Fails All 30 Jobs — ryanshrout · 2026-10-30
- TEM: Transformer Energy-Based Models Claim to Outscale Diffusion Without Guidance — du_yilun · 2026-10-30
- VisualForce: robots infer grip force from soft gripper deformation, no force sensors needed — du_yilun · 2026-10-30
- Microsoft Research: coding agents' real bottleneck is understanding code, not writing it — Microsoft Research · 2026-10-30