OpenAI claim summary for Math-2634
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
The displayed question has a negative answer under the manuscript's stated construction. Its counterexample meets the conditions in this problem and defeats the universal assertion, so this is a full disproof claim. The supporting results are manuscript 1 (family 100; 2026-09-27), manuscript 2 (family 100; 2026-09-27), manuscript 3 (family 100; 2026-09-27).
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Directionwise normalized cylinder-covering bound
OpenAI's claim
OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 100; 2026-09-27), the asserted result is that a regular tetrahedron has a finite covering by triangular-base cylinders whose total perpendicular area is strictly less than half its minimum projection area; In manuscript 2 (family 100; 2026-09-27), the asserted result is that radial segment sweeps have finite triangular-base cylinder realizations whose area converges to the weighted parameter cost, including a tetrahedral cover below the half-area bound; In manuscript 3 (family 100; 2026-09-27), the asserted result is that varying the axes of the standard two-cylinder tetrahedral cover yields a finite cover below the half-area threshold, also violating the directionwise normalized bound.Mathematical statement of the claimed result
Manuscript 1.
Put $H=\sqrt2$, $K=\{(x,y,Hs):0\le s\le1,\ |x|\le1-s,\ |y|\le s\}$ and $d(q)=(q^2+q^4)/16$; this tetrahedron has least projection area $H$. For small $\tau>0$, choose any finite partition $-1=q_0<\cdots<q_m=1$, coefficients $\alpha_j,\beta_j$ and positive continuous caps $R_j$ on $I_j=[q_{j-1},q_j]$. Require continuity of the piecewise affine $L(q)=\alpha_j-q\beta_j$ and $L(\pm1)=0$, and uniform estimates \[ \beta_j=q/2+O(\tau^2),\quad\alpha_j=(1+q^2)/4+O(\tau^2),\quad R_j(q)=1/2+\tau^2(d(q)+\eta)+O(\tau^4),\quad0<\eta<1/480. \] The constants are independent of $\tau,j,q$. Define $P_j^-=\{(0,qS,HS):q\in I_j,0\le S\le R_j(q)\}$, $P_j^+=\{(qT,0,H(1-T)):q\in I_j,0\le T\le R_j(q)\}$, and directions $v_j^-=(1,\tau\alpha_j,H\tau\beta_j)$, $v_j^+=(-\tau\alpha_j,1,H\tau\beta_j)$. The claimed finite cover is $K\subseteq\bigcup_j(P_j^-+\mathbb Rv_j^-)\cup(P_j^++\mathbb Rv_j^+)$, with compact perpendicular bases and total area \[ C_{\tau}/H=1/2+(2\eta-1/240)\tau^2+O(\tau^4)<1/2 \] for sufficiently small $\tau$. Constant caps give triangular bases; the threshold is independent of the number of intervals.Manuscript 2.
Choose a Euclidean plane $P$ with unit normal $e$, independent $a,b\in P$, $J=[\alpha,\beta]$ with $\alpha<\beta$, continuous $R\ge0$, a $C^1$ map $w:J\to P$, $p_0\in P$ and $L>0$. Set \[ \mathcal S=\{p_0+\rho(a+tb)+s(e+w(t)):t\in J,0\le\rho\le R(t),|s|\le L\}, \quad\mathcal A=|\det_P(a,b)|\int_{\alpha}^{\beta}\frac{R(t)^2}{2\sqrt{1+\|w(t)\|^2}}\,dt. \] If $w'(t)=\lambda(t)(a+tb)$ for continuous real $\lambda$, every tagged finite partition gives one covering cylinder per interval, with frozen axis $e+w(c_i)$ and nondegenerate compact triangular perpendicular base, whose total base area tends uniformly to $\mathcal A$ as the mesh tends to zero. Frozen projections of the actual interval sweeps give the same limit. The tetrahedral consequence claims, for each regular tetrahedron $K$ of positive edge length, a finite triangular-base cover with \[ \sum_i|B_i|<\tfrac12 A_{\min}(K),\qquad \sum_i\frac{|B_i|}{|\pi_{u_i^{\perp}}K|}<\tfrac12. \]Manuscript 3.
For every regular tetrahedron $K\subset\mathbb R^3$ of positive edge length, the claim supplies finitely many cylinders $B_i+\mathbb Ru_i$, with unit $u_i$, compact nondegenerate parallelogram bases $B_i\subset u_i^{\perp}$, covering $K$ and satisfying \[ \sum_i|B_i|<\tfrac12\min_{|u|=1}|\pi_{u^{\perp}}K|, \qquad\sum_i\frac{|B_i|}{|\pi_{u_i^{\perp}}K|}<\tfrac12. \] It also claims such finite covers with bounded open measurable bases. Both sums count base areas with multiplicity.Outline of the argument
For manuscript 1 (family 100; 2026-09-27), angularly tilted radial families receive a cubic buffer that preserves coverage. Secant-sector calculations give a negative quadratic area correction, and finite triangular enclosures retain the strict saving when the angular mesh is small.For manuscript 2 (family 100; 2026-09-27), one triangular enclosure is assigned to each interval of a tagged partition. Complementary shortened beams leave a strip covered by horizontal cylinders; exact overlap and strip calculations cancel the first-order cost and leave a strict second-order saving.
For manuscript 3 (family 100; 2026-09-27), tangential angular and rational slope fields preserve the relevant wedges. Complementary label displacements have a controlled second-order overlap surplus, so a small padding secures coverage while tilt lowers perpendicular area by a larger amount.
Formal verification
For manuscript 1 (family 100; 2026-09-27), OpenAI lists Lean statements for this assertion: a regular tetrahedron has a finite covering by triangular-base cylinders whose total perpendicular area is strictly less than half its minimum projection area.The central assertion is within the documented formal scope; the additional applications retain their own scope limits.
For manuscript 2 (family 100; 2026-09-27), OpenAI lists Lean statements for this assertion: radial segment sweeps have finite triangular-base cylinder realizations whose area converges to the weighted parameter cost, including a tetrahedral cover below the half-area bound.
The central assertion is within the documented formal scope; the additional applications retain their own scope limits.
For manuscript 3 (family 100; 2026-09-27), OpenAI lists Lean statements for this assertion: varying the axes of the standard two-cylinder tetrahedral cover yields a finite cover below the half-area threshold, also violating the directionwise normalized bound.
The central assertion is within the documented formal scope; the additional applications retain their own scope limits.
The linked family Comparator checks are CylinderCovering.lean, RuledCovering.lean, TriangularCovering.lean.
Their named declarations include OAI.CylinderCovering.fourPaperMain, OAI.RuledApproximation.fullMain, OAI.TriangularCovering.main.
This site has not executed the Lean code. Described statement coverage is not an independent proof check.
Status caveat
The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.Sources
- OpenAI, Finite angular cylinder covers below the half-area bound, 2026-09-27; citation key
OAI:Finite-angular-cylinder-covers-below-the-half-area-bound-September-27-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: ext:general-cap, ext:coefficient-hypotheses, ext:cap-hypothesis, ext:general-cost. - OpenAI, Finite triangular approximation of radial sweeps, 2026-09-27; citation key
OAI:Finite-triangular-approximation-of-radial-sweeps-September-27-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: cor:tetrahedron. - OpenAI, Slope-field perturbations of the two-cylinder covering, 2026-09-27; citation key
OAI:Slope-field-perturbations-of-the-two-cylinder-covering-September-27-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: c:main. - Family 100: Lean scope.
- Comparator CylinderCovering.json.
- Comparator CylinderCovering.lean.
- Comparator RuledCovering.json.
- Comparator RuledCovering.lean.
- Comparator TriangularCovering.json.
- Comparator TriangularCovering.lean.
- OpenAI catalogue entry.