What was already known
Anari and Rezaei’s Bethe analysis gave a deterministic (√2)ⁿ approximation for nonnegative matrices. Earlier Bethe inequalities reconstructed in this project are inputs, not the new bound.
AI involvement
Nima Anari supplied the high-level plan and guided the project. The disclosure credits ChatGPT 5.6 Sol Pro with the proof and Lean development, and reports Anari’s critical review of the result.
ChatGPT developed the retained proof and Lean formalization; Anari supplied the high-level attack and guidance, so the mathematical work is joint with a documented central model role.
- Supporting source (github.com) — Theorem statement, proof layers, axiom surface and manuscript status
- Supporting source (github.com) — Theorem 1 dependency and formalization map
Importance
Improves the stated exponential approximation base and supplies a binary polynomial-time implementation.
Limitations
The accompanying manuscript was still in preparation at the reviewed code version. The formal theorem covers the stated algorithm and complexity, while manuscript priority claims are outside the proof. No named human explanation of the full new proof mechanism is documented.
Technical verification
The cited repository reports a closed Lean theorem with no project-specific axioms or omitted proof obligations, including the finite-precision optimization routine and ordinary binary polynomial-time claim. Its metadata reports fresh Lean builds, an axiom audit, Comparator and kernel replay, plus Anari's critical author review. These are source-reported checks of the selected theorem, not checks reproduced in this review; manuscript priority claims are outside Lean.
Independent checking
Full Lean build, theorem dependency and axiom audit, Comparator statement comparison and kernel replay
- Checker
- Lean kernel and Comparator in the project-reported pinned build
- Scope
- BeyondBethe.theoremOne and the matching Palomar.beyond_bethe_permanent declaration: rational c^n approximation with c < sqrt(2) and ordinary binary polynomial time
- Basis
- Reported by the linked checker
Author verification and repeated critical mathematical passes over the listed proof components
- Checker
- Nima Anari, author-reviewer
- Scope
- Theorem 1, including its approximation statement, constants, boundary cases, reconstructed inputs, numerical algorithm and binary complexity claim
- Basis
- Reported by the linked checker
Human understanding
Anari's plan and verification show involvement and checking, and the repository maps proof components to Lean, but the reviewed sources do not provide a named human explanation of the full new mechanism. Few is the evidence default, not a finding that Anari understands little.
Correction and publication history
Improves the stated exponential approximation base and supplies a binary polynomial-time implementation.
Read this published revision