AI Proved What?

Episode 100, October 2026

Below half?

Finitely many cylinders cover the regular tetrahedron for less than half its smallest shadow

Covers result 100 in OpenAI’s catalog: all 4 papers. See its connections to other results and the work it cites.

6:34. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Planks and cylinders
  2. 1:50The claims
  3. 3:41How the cover works
  4. 5:49Where it stands

The claims, in plain words

A plank is the slab between two parallel planes. Tarski asked how thin a set of planks covering a convex body can be in total, and Bang proved that their widths add up to at least the body’s smallest width. Ball proved a sharper, direction-by-direction version for centrally symmetric bodies.

For cylinders in space, a cylinder is a flat base extended infinitely along the line perpendicular to it, and its cost is the area of that base. The yardstick is the body’s smallest shadow Amin, the least area of its orthogonal projections onto planes: one cylinder over that shadow covers the body at cost Amin. The regular tetrahedron does better. With edge 2, its smallest shadow is √2, seen along an edge, and two cylinders parallel to opposite edges, one below the middle height and one above, each over a triangle of area √2/4, cover it for exactly half. Bezdek recorded the question, attributed to Bang’s 1951 paper, whether every finite cylinder cover costs at least half the smallest shadow. A stronger version measures each base against the body’s shadow in that cylinder’s own direction: Bezdek and Litvak proved this relative cost is always at least 1/3, and at least 1 for ellipsoids, and Bezdek and Khan conjectured 1/2. Verreault’s 2026 survey lists the half-area question as open.

Result 100 is four OpenAI preprints dated September 27, 2026: the main paper (20 pages) and companions on finite approximation of ruled sets (12 pages), slope-field perturbations of the two-cylinder covering (23 pages) and triangular approximation of radial sweeps (28 pages). The main paper covers the regular tetrahedron of edge 2, for each tilt 0 < ε ≤ 1/2000, by 2⌈2/ε²⌉ cylinders with compact triangular bases whose total area, in units of the smallest shadow, is 1/2 − (13/6000)ε², with an error of at most 2ε⁴. That is below one half, so the half-area bound fails. The relative cost is unchanged by affine maps, so the directionwise conjecture fails for every tetrahedron. The slope-field and radial-sweep papers build their own counterexamples, with parallelogram and triangular bases.

What it doesn’t claim

The saving is tiny: at ε = 1/2000 the cover uses 16 million cylinders and saves about 5.4 × 10−10 of the smallest shadow. The papers do not improve the lower bound of 1/3 and do not say how low the cost can go, for the tetrahedron or for convex bodies in general; the best universal constant now lies between 1/3 and 1/2. For ellipsoids the answer was already settled.

Where it stands

Posted as preprints
OpenAI, four preprints dated September 27, 2026, released October 6
Peer reviewed
Not yet
Checked in Lean
OpenAI published Lean proofs of the regular-tetrahedron counterexamples and selected approximation theorems; we have not run the checks

Last checked October 19, 2026. The preprints have not been revised. OpenAI published Lean formalizations in three folders: the explicit triangular cover, with an unspecified error constant, in 9 files and 2,247 lines, matched against its comparator statement; selected ruled-set theorems and a further tetrahedron cover in 30 files and 4,303 lines; and 602 files and 64,073 lines proving selected statements of all four papers, including the explicit cover with the stated constants, matched against a combined statement. We found no unproved steps. The extension to every tetrahedron is outside the formalized statements. We have not run the checks. The papers are not among those OSVerify reviewed, and we have seen no expert review.

How the cover works

  1. Sectors with their own tilts. Each triangular base of the two-cylinder cover is cut into narrow sectors fanning out from its tip, labelled by slopes q from −1 to 1, at most ε² wide. Each sector gets its own axis, tilted in proportion to ε: (1, εαj, √2 εβj) for the lower family, with αj = (1 + qjqj+1)/4 and βj = (qj + qj+1)/4. A cylinder’s cost is the area of its base perpendicular to the axis, and tilting shrinks it by the factor 1/√(1 + ε²(αj² + 2βj²)).
  2. Matching the shared sides. The tilts are chosen so that the plane swept by a side shared by two neighbouring sectors is the same for both: y = qt + εx(1 − q²)/4. At any point of the tetrahedron these planes give a list of positions starting at −t and ending at t, where t is the height scaled to run from 0 to 1; some adjacent pair brackets the point, even if the list is out of order, so a sector in each family is aimed at it.
  3. Margins. Each sector is extended past the middle height by ε² times 1/1000 plus the largest value of q²(1 + q²)/16 on the sector. Near the middle the two families’ heights shift by −εxy and +εxy, so the first-order shifts cancel, and the margins close the second-order gaps. Per ε², tilting saves 17/240 and the margins cost 103/1500, leaving a net saving of 13/6000.

The numbers in the video

  • The tetrahedron’s shadow formula agrees with convex hulls of projected vertices; the smallest shadow is √2 ≈ 1.414, along an edge, and the shadow from above is 2.
  • Summing the base areas of the tilted cover, divided by the smallest shadow, gives 1/2 − 2.153 × 10−7 at ε = 1/100 (40,000 cylinders) and 1/2 − 5.41658 × 10−10 at ε = 1/2000 (16 million cylinders), against (13/6000)ε² = 5.41667 × 10−10.
  • Sampling 200,000 points (40,000 of them from the middle band) at tilt 1/20: none missed with the margins, 298 missed without them, all with heights between 0.488 and 0.511. With the margins, a few points were still missed at tilts 1/10 (4) and 1/5 (22); the proof takes ε ≤ 1/2000.
  • The exact coefficients: 17/240 − 103/1500 = 13/6000; without the fixed 1/1000 in the margin, the saving would be 1/240.

Read the source

The 4 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00Planks and cylinders

Cover a convex body with planks, the slabs between pairs of parallel planes. Tarski asked how thin they can be in total. Bang proved that the widths must add up to at least the body’s smallest width: no arrangement of planks beats a single plank laid across the narrowest direction. Ball later proved a sharper, direction-by-direction version for centrally symmetric bodies, where each plank’s width is divided by the body’s width in the same direction, and the sum is still at least one. Now cover a body in space with cylinders. A cylinder here is a flat base, extended along the line perpendicular to it, infinitely in both directions. Its cost is the area of its base. Let A_min be the body’s smallest shadow, the least area of its projections onto planes. One cylinder over that shadow covers everything, at cost A_min. For the regular tetrahedron, two cylinders do it for half as much. With edge 2, its smallest shadow is √2, seen along an edge. Two cylinders parallel to opposite edges, one covering everything below the middle height and one everything above, each have a triangle of area √2/4 as base. So does every finite cylinder cover cost at least half the smallest shadow? Bezdek recorded this question, attributing it and the tetrahedron example to Bang’s 1951 paper. A stronger version divides each base by the body’s shadow in that cylinder’s own direction. Bezdek and Litvak proved that this relative cost is always at least 1/3, and at least 1 for ellipsoids. Bezdek and Khan conjectured 1/2. Verreault’s 2026 survey lists the half-area question as open. The tetrahedron’s two-cylinder cover sits exactly on the line.

1:50The claims

Result 100 is four OpenAI preprints, all dated September 27. The main one, 20 pages, covers the regular tetrahedron of edge 2 by finitely many cylinders with triangular bases. For each small tilt ε, at most 1/2000, it uses 2⌈2/ε²⌉ cylinders. Measured in units of the smallest shadow, their total base area is 1/2 − (13/6000)ε², with an error of at most 2ε⁴. That is below 1/2, so the half-area bound fails. The relative cost does not change under affine maps, so the stronger directionwise conjecture fails for every tetrahedron. The saving is tiny. At ε = 1/2000, the cover uses 16 million cylinders and saves about 5.4 × 10⁻¹⁰ of the smallest shadow. The papers do not improve the lower bound of 1/3, and do not say how low the cost can go. Three companions, of 12, 23 and 28 pages, give a way to turn smooth families of segments, whose directions vary in a controlled way, into finite cylinder covers with almost no extra cost; covers with parallelogram bases; and triangular covers of radial sweeps. The last two also build their own tetrahedron counterexamples. OpenAI published Lean formalizations: the explicit triangular cover, with a looser error constant, in 9 files, about 2,200 lines; a segment-family theorem and a further tetrahedron cover in 30 files; and a combined statement of selected results from all four papers, with the stated constants, in about 600 more files and 64,000 lines. We have not run the checks.

3:41How the cover works

Start from the two-cylinder cover. Cut each triangular base into narrow sectors fanning out from its tip, labelled by slopes q from −1 to 1, and give each sector its own axis, tilted by an amount proportional to ε. The cylinder’s cost is the area of its base perpendicular to the axis, and tilting shrinks it by the factor 1/√(1 + tilt²). That is the saving. The danger is gaps: between neighbouring sectors, and between the two families. Neighbouring sectors are handled by matching. Each sector’s tilt is chosen so that the plane swept by a shared side is the same for both sectors that share it. At any point of the tetrahedron, these planes give a list of positions starting at −t and ending at t, where t is the point’s height, scaled so the tetrahedron runs from 0 to 1. Some adjacent pair brackets the point, even if the list is out of order, so some sector in each family is aimed at it. What remains is reach: near the middle height, each family’s sectors could stop just short. So every sector is extended past the middle by ε² times a margin: 1/1000 + the largest value on the sector of q²(1 + q²)/16. Near the middle, the two families’ heights shift by −εxy and +εxy, so the first-order shifts cancel and the margins close what is left. In our check at tilt 1/20, without the margins 298 of 200,000 sampled points were missed, all near the middle; with them, none. At larger tilts a few points still slipped through even with the margins, so the tilt really must be small; the proof takes it at most 1/2000. Per ε², tilting saves 17/240, the margins cost 103/1500, and the difference is 13/6000. Summing all 16 million base areas at ε = 1/2000, we found a saving that matches 13/6000 of ε² to four digits.

5:49Where it stands

The four preprints are not peer reviewed and have not been revised. Lean covers the regular-tetrahedron counterexamples and selected forms of the approximation theorems, but not the step to every tetrahedron; we have not run it. They are not among the papers OSVerify reviewed, and we have seen no expert review. If it holds, the classic two-cylinder cover of the regular tetrahedron is not the cheapest: many slightly turned cylinders cover it for a little less than half its smallest shadow. How low the cost can go for the tetrahedron remains open, and so does the best bound for all bodies, which now lies between 1/3 and 1/2.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.