{"id":"palomar/PALOMAR-2026-08-29-000006","url":"https://github.com/nimaanari/formalization-beyond-bethe/tree/325cda6d2118870f7f121a9a986b7ea9ffdd7a26","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000006-v1.json","repo":"https://github.com/nimaanari/formalization-beyond-bethe","tags":["cs.DS","math.CO","msc:68W25","msc:15A15","permanent-approximation","algorithms","lean-formalization","counting"],"score":0,"title":"nimaanari/formalization-beyond-bethe","trust":"high","domain":"cs.DS","source":"palomar","authors":["Nima Anari"],"reviews":0,"subject":"cs.DS","summary":"Computing or approximating the permanent is a canonical problem in theoretical computer science and in counting and sampling. Before this work, the canonical Bethe approximation gave the best known deterministic guarantee, with approximation factor (sqrt 2)^n. This formalization proves that there is an absolute constant c < sqrt 2 and a deterministic polynomial-time c^n-approximation for every nonnegative rational matrix. It checks the mathematical and algorithmic proof down to Lean's standard logical axioms, including the finite-precision convex-optimization implementation.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-08-29","reactions":{},"formalized":true,"formalizes":[{"title":"Beyond the Bethe Approximation of the Permanent","identifier":"","relationship":"formalizes"}]}