Convex and discrete geometry

The Lean Pool projects whose card's first MSC2020 code is in class 52, Convex and discrete geometry: 15 articles, one per card.

TheoremA Conditional Fourteen-Point Case of Erdős Problem 132#

Formalizes the planar Hopf--Pannwitz diameter bound and proves the fourteen-point low-multiplicity conclusion conditional on exactly two remaining published interfaces: the known maximum-cardinality bound for planar sets with at most six distances and the Szöllősi--Östergård classification of thirteen-point planar six-distance sets. Internally derives the exact failure profile and endpoint deletion, constructs the three classified templates, eliminates the nonregular cases by multiplicity, and excludes the regular tridecagon extension by explicit second and fourth moments. The general Erdős problem remains open.

Quoted from the card LeanPool/projects/erdos132-n14.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • LeanPool.Erdos132N14.hopfPannwitzLowMultiplicityDistance14 (theorem), declared in LeanPool/Erdos132N14/HopfPannwitz.lean, line 292: “Every injectively labelled fourteen-point planar configuration has a realized distance represented by at most fourteen unordered pairs; the proof chooses that distance to be a diameter.” Its source, as the card gives it: “The planar diameter bound, conventionally associated with Hopf--Pannwitz; Perles's clockwise-extreme endpoint proof.”
  • LeanPool.Erdos132N14.erdos132_for_fourteen_of_published_inputs (theorem; a main declaration), declared in LeanPool/Erdos132N14/Main.lean, line 468: “Assuming precisely the published planar few-distance cardinality and Szöllősi--Östergård classification interfaces, every injectively labelled fourteen-point planar configuration realizes at least two distances whose unordered-pair multiplicities are at most fourteen.” Its source, as the card gives it: “Erdős Problem 132; Hopf--Pannwitz's planar diameter bound; Wei, "A Proof of Erdős--Fishburn's Conjecture for g(6)=13," EJC 19(4) P38 (2012), doi:10.37236/2917; Szöllősi--Östergård, EJC 27(1) P1.23 (2020), Table 1 and Theorem 16, doi:10.37236/8565.”
Project
Sources
LeanLeanPool.Erdos132N14.erdos132_for_fourteen_of_published_inputs

TheoremThe Bannai-Bannai-Stanton Bound on Distance Sets#

Formalizes the Bannai-Bannai-Stanton theorem: a distance set S in ℝ^d realizing s distinct distances has size at most Nat.choose (d + s) s. Follows the short polynomial-method proof of Petrov and Pohoata via a generalized Croot-Lev-Pach rank lemma, with auxiliary results on the diagonal linear-independence argument for polynomials, monomial counting of bounded degree, and a rank bound for sums of matrices.

Quoted from the card LeanPool/projects/bannai-bannai-stanton.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanBannaiBannaiStanton.bannai_bannai_stanton_bound

TheoremConvex Three-Distance Degree-Six Theorem and Exceptional-Word Closures#

Proves that every finite cyclically strictly convex planar configuration has a vertex incident to at most six edges from its three largest distance classes. The proof selects a maximal-gap vertex and coordinated majorants, closes all exceptional inner branches, performs the five-row enumeration, and transports all thirteen canonical cover words to four shared full-two-rung, anti-saturation, terminal-cage, and four-edge-cage predicates. It also proves exceptional-count rigidity and an explicit heptagon refutation of a tempting stronger majorant claim, with rational regression witnesses. This settles the all-n k=3 instance of the paper's suggested degree-2k convex bound; Morić--Pritchard proved the corresponding top-three edge bound for sufficiently large n. It does not settle the general-k suggestion or the general Erdős problem 132.

Quoted from the card LeanPool/projects/erdos132-convex-k3.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 11 main results, each with its informal statement quoted from the card. The scan finds 11 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.Erdos132ConvexK3.convex_top_three_degree_six

TheoremConway–Soifer covering conjecture for n = 3#

Proves that ten congruent closed equilateral triangles covering a filled equilateral triangle of side three have common side at least one, with arbitrary positions, rotations and overlaps. Consequently ten unit triangles cannot cover a triangle of side 3 + ε for ε > 0. Includes reusable finite halfspace and ray-endpoint geometry, orientation-independent support and area bounds, and verified Bernstein polynomial interval checkers. Four derived contact cases and 100 kernel-checked certificates close the proof without a certificate hypothesis.

Quoted from the card LeanPool/projects/conway-soifer-three.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • ConwaySoifer.ten_triangle_cover_lower_bound (theorem; a main declaration), declared in LeanPool/ConwaySoifer.lean, line 640: “Any ten congruent closed equilateral triangles covering the filled equilateral target of side three have common side at least one. Positions, rotations and overlaps are unrestricted.” Its source, as the card gives it: “Public v1.0.0 release, 2026-09-11T17:12:25Z; upstream README and Geometry/Basic.lean.”
  • ConwaySoifer.no_ten_unit_triangle_cover (theorem), declared in LeanPool/ConwaySoifer.lean, line 643: “For every ε > 0, ten closed equilateral triangles of side one cannot cover the filled equilateral target of side 3 + ε, regardless of position or rotation.” Its source, as the card gives it: “Upstream public theorem and its proved scaling corollary.”
Project
Sources
LeanConwaySoifer.ten_triangle_cover_lower_bound

TheoremEhrhart's sharp volume inequality#

Proves Ehrhart's sharp upper bound for the volume of a centered full-dimensional convex body whose origin is its unique interior lattice point. The development builds the weighted complex-analytic and variational machinery needed for the bound and verifies sharpness using the centered simplex, including its barycenter and exact volume.

Quoted from the card LeanPool/projects/ehrhart-volume-inequality.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanEhrhart.Volume.ehrhart_volume_inequality_for_sets

TheoremEqual-area and equal-perimeter convex partitions#

Formalizes the Akopyan–Avvakumov–Karasev theorem that every planar convex body can be partitioned into any prescribed positive number of convex pieces with equal area and equal perimeter. Area is Lebesgue measure and perimeter is Hausdorff measure of the boundary.

Quoted from the card LeanPool/projects/nrr-aak.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanHumanVerification.equalAreaEqualPerimeterPartition

TheoremThe Erdős–Tuza–Valtr conjecture#

Formalizes the Erdős–Tuza–Valtr conjecture, a sharp refinement of the Erdős–Szekeres happy-ending theorem, proving that any general-position point set of size at least C(n+2,2)+2 contains the target cup–cap configuration.

Quoted from the card LeanPool/projects/erdos-tuza-valtr.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanErdosTuzaValtr.main · Config.main_lemma

LemmaFinitely generated cones and finite LP duality#

Proves that finitely generated cones in real normed spaces are closed, including a conic Carathéodory reduction and PointedCone API forms. Derives a finite-dimensional inequality form of Farkas' lemma and proves packing attainment with equality to the covering infimum for finite covering and packing linear programs. The Farkas and LP statements overlap the pooled Duality development; the generic cone-closedness results provide the project's distinct reusable API.

Quoted from the card LeanPool/projects/erdos81-paper-i-contrib.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.Erdos81PaperIContrib.fg_cone_isClosed

TheoremThe main theorem of polytopes#

Formalizes the Minkowski–Weyl theorem — the equivalence between V-polytopes (convex hulls of finite point sets) and bounded H-polytopes (finite intersections of half-spaces) in a finite-dimensional real vector space.

Quoted from the card LeanPool/projects/main-theorem-of-polytopes.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanMainTheoremOfPolytopes

TheoremMonsky's Theorem#

Formalizes Monsky's theorem that a square can be dissected into n triangles of equal area if and only if n is nonzero and even, via a 2-adic valuation, a three-coloring of the unit square, and a rainbow-triangle argument.

Quoted from the card LeanPool/projects/monsky.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.Monsky.monsky_theorem

TheoremOptimality of Gerver's sofa#

Formalizes Baek's solution of the moving sofa problem: Gerver's sofa attains the supremum of the areas of closed connected shapes that can move continuously around a right-angled corner in a unit-width hallway. Includes certified Gerver parameters, admissibility, convex cap geometry, Stieltjes curve area, Jordan separation, polygon approximation, and the concave quadratic upper bound.

Quoted from the card LeanPool/projects/moving-sofa.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanMovingSofa.sofaConstant_eq_volume_gerversSofa

TheoremPeriod Lengths of Rational Cut-and-Project Gap Sequences#

Formalizes the closed-form minimal periods of one-dimensional rational cut-and-project gap sequences at the level of the paper's residue model, plus a fully geometric aperiodicity theorem for irrational slopes. For coprime α, β ∈ ℕ and window parameter ω ≥ 0, write N = ⌊ωα⌋ + ⌊ωβ⌋ + 1 and D = α² + β². The strip-to-residue reduction of the paper — sorting the hits of the length-N progression twisted by the geometric multiplier −αβ⁻¹ (mod D) — is taken as the definition of the gap sequence rather than derived from the lattice; for it, the multiset convention has minimal period N/D when D ∣ N and N otherwise, and the set convention (multiplicities flattened to {0,1}) has minimal period 1 when N ≥ D and N otherwise. The irrational case is geometric from first principles: for positive irrational slope and ω > 0, the accepted points of ℤ² sorted by the physical projection have a gap sequence with no finite period, via injectivity of the projection and Kronecker density of the internal image.

Quoted from the card LeanPool/projects/cut-and-project.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanCutAndProject.main_theorem_geometric_concrete

TheoremPlanar Point Sets Whose Non-Diameter Distances Form a Geometric 3-Chain#

Formalizes a support theorem about planar point sets whose non-diameter squared distances are confined to a geometric progression of ratio three. The chain-quadruple theorem shows that no planar quadruple with all six squared distances in such a chain can span two chain steps, and classifies the seven labelled patterns that do occur: the rhombus of two glued equilateral triangles, in five positions of its long edge, and the equilateral triangle with its centroid, in two. A Gram obstruction then rules out any five-point chain configuration. The lift to n at least thirteen runs through the diameter graph: the Caro--Wei independence bound, proved here, produces an independent five-set once the diameter graph is known to have at most as many edges as the set has points. That edge bound is the Hopf--Pannwitz theorem of 1934, and it already exists in the pool; this project reproves it in its own model as a supporting lemma, claiming no novelty for it, and the overlap is set out in full below. The result is unconditional. There is no prior write-up behind this development. The restriction to ratio 3 is ad hoc: the 3-chain statement was produced by the author's automated research pipeline in August 2026, while the cited source poses the ambient Erdos problem and does not state this restriction or result. This theorem does not resolve Erdos 132, whose distance spectra need not be geometric 3-chains. The descriptive labels used in the Lean docstrings are internal to this development and refer to no numbered result elsewhere. Overlap disclosure. Erdos132ThreeChain.hopfPannwitz is NOT offered as a new result. The pooled project Erdos132N14 already contains the same diameter bound, and the version here exists only so that this project is self-contained. Its statement, verbatim from LeanPool/Erdos132N14/HopfPannwitz.lean, is

theorem diameterEdges_card_le (P : Configuration ι) (S : Finset ι) {d : ℝ} (hd : 0 < d) (hmax : ∀ f ∈ pairs S, P.pairDistance f ≤ d) : (diameterEdges P S d).card ≤ S.card

where, from LeanPool/Erdos132N14/Basic.lean, Configuration ι is a structure carrying an injective point : ι → ℂ, pairs S = (S ×ˢ S).filter fun e ↦ e.1 < e.2 for a LinearOrder ι, pairDistance P e = dist (P.point e.1) (P.point e.2), and diameterEdges P S d = (pairs S).filter fun e ↦ P.pairDistance e = d. The corresponding statement here is

theorem hopfPannwitz {X : Finset Point} {D : ℝ} (hD : IsSqDiameter X D) : ∑ v ∈ X, degree (DiameterAdj D) X v ≤ 2 * X.card

with Point = ℝ × ℝ, sqDist the squared Euclidean distance, DiameterAdj D p q = (p ≠ q ∧ sqDist p q = D), degree adj X v = (X.filter (adj v)).card, and IsSqDiameter X D asserting that D is realised by two distinct points of X and dominates every squared distance inside X. The two are the same mathematical theorem — a positive maximal distance is realised at most as often as there are points — carried by different models: an injective map from a linearly ordered index type into the complex plane, counting a Finset of unordered pairs, against a Finset of points of the real plane, in squared distances and degree-sum form. Neither statement is an instance of the other without a model bridge: a LinearOrder on ℝ × ℝ, a dist-to-sqDist transfer, and a handshake lemma. The proofs differ too, Perles charging there against pendant deletion driven by Cramer's rule here. No project in the pool imports another, and CONTRIBUTING.md records that independence as the property the fast per-project build relies on, so this project reproves the bound rather than importing it. It is a supporting lemma of this development, not one of its results, and it is therefore not listed among the main results below. Two supporting identities also exist elsewhere in the pool. From LeanPool/Erdos97ConvexOctagon/CayleyMenger.lean,

theorem cm4_sqDist_eq_zero (a b c d : Plane) : cm4 (sqDist a b) (sqDist a c) (sqDist a d) (sqDist b c) (sqDist b d) (sqDist c d) = 0

over Plane = EuclideanSpace ℝ (Fin 2) is the same four-point Cayley--Menger vanishing as this project's

theorem gramDet_eq_zero (a b c d : Point) : gramDet (sqDist a b) (sqDist a c) (sqDist a d) (sqDist b c) (sqDist b d) (sqDist c d) = 0

over Point = ℝ × ℝ; both are one-line ring identities in the coordinates. From LeanPool/DistanceGeometry/SchoenbergHard.lean,

theorem schoenberg {D : Matrix (Fin n) (Fin n) ℝ} (hD : IsPreDistMatrix D) : EmbedsIn D k ↔ (centeredGram D).PosSemidef ∧ (centeredGram D).rank ≤ k

characterizes Euclidean distance matrices in general dimension. This project never invokes it: the four-point condition is used directly as a ring identity and the five-point obstruction is a sum-of-squares contradiction, so no positive-semidefiniteness criterion is needed.

Quoted from the card LeanPool/projects/erdos132-three-chain.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 8 main results, each with its informal statement quoted from the card. The scan finds 8 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • Erdos132ThreeChain.nonDiameterSqDists_ne_chain (theorem; a main declaration), declared in LeanPool/Erdos132ThreeChain/Statement.lean, line 56: “Let n be at least thirteen, let a be positive, and let X be a finite set of points of the real plane with exactly n elements. Suppose D is the squared diameter of X, meaning that D is realised by two distinct points of X and dominates every squared distance inside X. Then for every natural number h, the set of squared distances realised by distinct points of X and different from D is not equal to the geometric 3-chain consisting of a times 3^j for j below h.”
  • Erdos132ThreeChain.four_chain_adjacent (theorem), declared in LeanPool/Erdos132ThreeChain/Support.lean, line 74: “Let a be positive and let S be a four-element set of points of the real plane such that every squared distance between distinct points of S equals a times a nonnegative power of three. Then there is a positive r, itself equal to a times a nonnegative power of three, for which every squared distance between distinct points of S equals r or 3r.”
  • Erdos132ThreeChain.pair_classification (theorem), declared in LeanPool/Erdos132ThreeChain/FourPoints.lean, line 299: “Let c be positive and let A, B, C, D be points of the real plane with the squared distance from A to B equal to c and every other pairwise squared distance equal to c times a nonnegative power of three. Then each of the four squared distances from A and B to C and to D equals c or 3c, at least one of the two squared distances from A and B to C equals c, likewise for D, the squared distance from C to D equals c or 3c, the squared distance from A to C equals c or that from B to D equals c, the squared distance from B to C equals c or that from A to D equals c, and the whole labelling is one of exactly seven explicit patterns: five with a single edge of squared length 3c, and two in which the three edges of squared length 3c form a triangle.”
  • Erdos132ThreeChain.no_five_chain_finset (theorem), declared in LeanPool/Erdos132ThreeChain/Support.lean, line 134: “Let a be positive. There is no five-element set of points of the real plane in which every squared distance between distinct points equals a times a nonnegative power of three.”
  • Erdos132ThreeChain.no_four_on_circle (theorem), declared in LeanPool/Erdos132ThreeChain/FivePoints.lean, line 64: “Let c be positive. There are no four points of the real plane, each at squared distance c from a common point, whose six pairwise squared distances all equal c or 3c.”
  • Erdos132ThreeChain.carowei (theorem), declared in LeanPool/Erdos132ThreeChain/CaroWei.lean, line 52: “Let adj be a symmetric irreflexive relation with decidable adjacency on a type, and let V be a finite set of vertices. Then V has a subset S, no two elements of which are adjacent, whose cardinality is at least the sum over v in V of one divided by one plus the number of neighbours of v inside V.”
  • Erdos132ThreeChain.exists_independent_five (theorem), declared in LeanPool/Erdos132ThreeChain/CaroWei.lean, line 126: “Let adj be a symmetric irreflexive relation with decidable adjacency on a type, and let V be a finite set of at least thirteen vertices whose degrees inside V sum to at most twice the cardinality of V. Then V has a five-element subset no two elements of which are adjacent.”
  • Erdos132ThreeChain.chainTwo_nonDiameter_support (theorem), declared in LeanPool/Erdos132ThreeChain/Witnesses.lean, line 77: “There is a five-element set of points of the real plane whose squared diameter is 4 and whose set of non-diameter squared distances is exactly the two-term geometric 3-chain consisting of 1 and 3. The configuration that the headline forbids for at least thirteen points is therefore realisable at five points with chain length two.”
Project
Sources
LeanErdos132ThreeChain.nonDiameterSqDists_ne_chain

TheoremThe Rupert Problem for convex polyhedra#

Formalizes the Rupert property for the cube, the regular tetrahedron, and the triakis tetrahedron, exhibiting for each an explicit straight-through hole admitting a congruent copy.

Quoted from the card LeanPool/projects/rupert.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanCube.rupert · Tetrahedron.rupert · TriakisTetrahedron.rupert

TheoremSharp asymptotic upper bounds for sphere packing#

Formalizes the sharp high-dimensional asymptotics of the unrestricted Cohn--Elkies linear program and bridges them to sphere-packing density. The development constructs radial test functions through Mellin, saddle-point, and harmonic analysis, proves radialization preserves the unrestricted optimum, and certifies the exact natural- and base-two exponential rates.

Quoted from the card LeanPool/projects/sphere-packing.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
  • Authors: OpenAI, Sidharth Hariharan, Gareth Ma, Dean Cureton.
  • Source: Ten Advances in Mathematics and Theoretical Computer Science by OpenAI.
  • Project repository: openai/ten-proofs, at commit 94bc0feb.
  • Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
  • License: Apache-2.0.
  • MSC2020: 52C17, 41A60, 42A38.
  • In Lean Pool: LeanPool/SpherePacking, from the card LeanPool/projects/sphere-packing.yaml.
Sources
LeanPackingBounds.sharpFullCohnElkiesManuscriptConclusions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.