Petty’s projection-volume conjecture in dimensions at least four

Formalization

• OpenAI math release, Lean scope notes for family 088 (lean/docs/088.md, release of 2026-10-06). States that the formalization covers the inequality with ellipsoid equality for every convex body and every n ≥ 4 (comparator statement PettyProjectionVolume.lean), while the other projection-body inequalities (the consequences in Section 7) are excluded. [family-level]
• anxkhn, Add Petty's unpolarized projection-volume inequality (google-deepmind/formal-conjectures issue #7145, opened 2026-10-11, open). Proposes adding Theorem 1.1 (n ≥ 4, arbitrary convex bodies, equality for affine ellipsoids) as a formal statement, sourced from this paper.
• anxkhn, feat(Paper): add Petty's projection-volume inequality (google-deepmind/formal-conjectures PR #7150, opened 2026-10-11, open, one approving review 2026-10-12). Adds the statement and a shared ProjectionBody definition without a proof; the approving reviewer states it matches Theorem 1.1 of the manuscript, and no formal_proof attribute is proposed.

Possibly relevant literature (found by the agent, not checked)

• Z. Mustafaev, Some geometric inequalities for the Holmes–Thompson definitions of volume and surface area in Minkowski spaces (J. Inequal. Pure Appl. Math. 5 (2004), no. 1, Art. 17). Relates Petty's conjecture to the equality case of a lower bound for Holmes–Thompson surface area over volume of the unit ball, the setting of the paper's Holmes–Thompson isoperimetry corollary (Section 7).
• H. Martini and Z. Mustafaev, On unit balls and isoperimetrices in normed spaces (Colloq. Math. 127 (2012), no. 1, 133ff., doi:10.4064/cm127-1-10). Discusses whether homothety of the unit ball and the Holmes–Thompson isoperimetrix forces an ellipsoid and proves an estimate related to Petty's conjectured projection inequality; relevant to the equality conclusion of the Holmes–Thompson corollary (the paper cites only Martini–Mustafaev 2008).
• C. Saroglou, Volumes of projection bodies of some classes of convex bodies (Mathematika 57 (2011), no. 2, 329–353, doi:10.1112/S0025579311001860). Earlier partial results on Petty's minimum problem for |ΠK|/|K|^{n-1}, relevant to the paper's survey of previous results (which cites Saroglou 2015 only).