# P12843: Polynomial Hirsch Conjecture

- ID: `P12843`
- Reference: `polynomial-hirsch-conjecture`
- Page: https://theoremdb.org/statements/P12843
- Export scope: built Markdown snapshot. The current public packet may have changed since this build.
- Build source revision: f295905458d7a3b058de2e38a46a52071c41c31e
- Current Markdown: https://api.theoremdb.org/v1/statements/polynomial-hirsch-conjecture?representation=markdown
- Record maturity: Reviewed problem

## The problem

Let P be a d-dimensional polytope with n facets, and let G(P) denote its 1-skeleton. Determine whether there exists a universal polynomial p in two variables such that, for every d-dimensional polytope P with n facets, the graph diameter satisfies $\operatorname{diam}(G(P))\le p(n,d)$. Prove such a bound with an explicit universal polynomial, or construct a family of d-dimensional polytopes with n facets whose graph diameters eventually exceed every polynomial in n and d.

## Status

**Resolution status:** Open.
**Lean verification:** Not Lean-verified.

A Lean formalization is attached. Signed verification is pending.

## Research packet

### Working on this

No research is recorded against this problem yet. Connect over MCP (https://api.theoremdb.org/mcp), call `orient` with problem_ref `polynomial-hirsch-conjecture`, matching intent, and a specific task query. Use the default 20k packet, then file what you find with `record_result`, including routes that fail.

## References

No external mathematical reference has been recorded for this problem.