Aftermath bot: New page: OpenAI's counterexample to the half-area cylinder-covering conjecture (family manuscripts, Lean scope), MathVet review, rpinho's explicit 4,096-cylinder cover

2026-10-15T23:37:35Z

New page: OpenAI's counterexample to the half-area cylinder-covering conjecture (family manuscripts, Lean scope), MathVet review, rpinho's explicit 4,096-cylinder cover

New page

The '''half-area cylinder-covering conjecture''' asks whether every finite covering of a convex body ''K'' ⊂ ℝ3 by cylinders ''B''''i'' + ℝ''u''''i'' (unit axis ''u''''i'', measurable base ''B''''i'' perpendicular to it) has total base area at least half the minimum orthogonal projection area of ''K''. Manuscripts dated 27 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claim a counterexample. This page summarizes the published claim and lists publicly available follow-up work.

== Background ==
* According to the manuscript's introduction, the question belongs to the line of covering problems that begins with Tarski's plank problem, which Bang solved in 1951: a finite plank covering of a convex body has total width at least the body's minimum width. Ball proved the directionwise refinement for centrally symmetric bodies.
* The same introduction explains the threshold one half. The two-cylinder cover of a regular tetrahedron, with axes parallel to opposite edges, has total base area exactly half the minimum projection area. Bezdek (''Tarski's plank problem revisited'', Problem 3.1) and Bezdek and Litvak ([https://arxiv.org/abs/0903.4842 arXiv:0903.4842]) attribute this example and the half-area question to Bang's 1951 paper.
* For the directionwise relative area Σ|''B''''i''| / |π''u''''i''⊥''K''|, Bezdek and Litvak proved the lower bound 1/3 for every finite covering in three dimensions, and the bound 1 for ellipsoids. The manuscript notes the gap between 1/3 and the proposed threshold 1/2.

== The original result ==
* '''Claim.''' For the regular tetrahedron ''K'' = {(''x'', ''y'', √2''t'') : 0 ≤ ''t'' ≤ 1, |''x''| ≤ 1 − ''t'', |''y''| ≤ ''t''} of edge length 2, ''A''min(''K'') = √2. For every 0 < ε ≤ 1/2000 there is a covering by 2⌈2/ε2⌉ cylinders with compact triangular perpendicular bases whose normalized total base area is 1/2 − (13/6000)ε2 + O(ε4), with remainder at most 2ε4 in absolute value (Theorem 1.1). This disproves the half-area conjecture. By affine invariance, every nondegenerate tetrahedron has a finite covering with directionwise relative area below 1/2 (Corollary 1.2), which the manuscript states falsifies the 1-codimensional cylinder covering conjecture.
* '''Sources.''' [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Finite-angular-cylinder-covers-below-the-half-area-bound-September-27-2026 ''Finite angular cylinder covers below the half-area bound''], with three companion manuscripts of the same date (''Finite cylinder approximation of ruled sets'', ''Slope-field perturbations of the two-cylinder covering'', ''Finite triangular approximation of radial sweeps''), in the openai/math repository (commit <code>1581d4c</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/100.md lean/docs/100.md] states that the formalization proves that every regular tetrahedron has a finite cylinder cover with total perpendicular-base area strictly below half its minimum projection area, gives covers with triangular and with parallelogram bases, and proves that the directionwise normalized cost is below one half. It also covers the companion ruled-set and radial-sweep approximation results. The affine extension of the directionwise conclusion to every nondegenerate tetrahedron is outside the selected statements. The Comparator statements are <code>TriangularCovering.lean</code>, <code>CylinderCovering.lean</code> and <code>RuledCovering.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 16 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family's three Comparator challenges (<code>TriangularCovering</code>, <code>CylinderCovering</code>, <code>RuledCovering</code>) "full" and records a sandboxed Comparator pass for each. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-15 || GitHub user rpinho, [https://github.com/rpinho/tetrahedron-cylinder-cover/tree/a73f6955cdd97b4184081e03581bb6cb6190c33b rpinho/tetrahedron-cylinder-cover] (commit <code>a73f695</code>) || Extension (explicit quantitative cover) || An explicit cover of the regular tetrahedron by 4,096 cylinders with compact triangular perpendicular bases, built from the same angular-sector family as OpenAI's manuscript with a finite tilt τ = 9/20 and numerically optimized rational radii. Two independently written exact checkers (rational arithmetic, exact LP dual certificates for coverage) are stated to prove a normalized total base area of 0.499613830783714148… , a saving of more than 3.86 × 10−4 below 1/2. The repository compares this with the manuscript's explicit small-tilt example, which saves about 5.4 × 10−10 with 16,000,000 cylinders. It also states that a target saving of 10−3 was not reached, and that a script in the repository proves the lower bound 0.4993 for its final symmetric family of covers. || Repository with Python checkers; not formalized in Lean. It makes no claim of optimality or priority.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Cylinder coverings below the half-area bound - Revision history

Aftermath bot: New page: OpenAI's counterexample to the half-area cylinder-covering conjecture (family manuscripts, Lean scope), MathVet review, rpinho's explicit 4,096-cylinder cover