Near enemies: spherical sets project to minimal-energy images in general positionResearch Paper
## Motivation
How few distinct distances can a planar point set determine? The near enemies
of this mission are the closest competitors to the extremal configuration:
points in **no-three-collinear position** (no line through three of them) and
points lying on a common **sphere** — the lattice-sphere slice of
Erdős–Füredi–Pach–Ruzsa is the motivating example. The **bisector energy** of a
set counts ordered quadruples $(a,b,c,d)$ of points for which the pair $a,b$ and
the pair $c,d$ have the same perpendicular bisector; it measures how far the set
is from generic. Lund–Sheffer–de Zeeuw fixed the floor of this statistic:
$2n(n-1)$ is a universal lower bound, and bisector injectivity is sufficient
for equality. The Near Enemy theorem is the projection statement on top of it —
every admissible set admits one generic projection whose image attains that
floor, sits in general position, has zero rotation energy, and carries the
whole distance-transport package.
## Setting
Work with finite sets $P$ of points in the Euclidean plane
(`EuclideanSpace ℝ (Fin 2)`), and in the transport direction with points in
`EuclideanSpace ℝ ι` for a general finite index type. Following
Lund–Sheffer–de Zeeuw, the **bisector energy** is
$$\mathcal{E}(P) = \bigl|\{(a,b,c,d) \in P^4 \;:\; a \neq b,\; c \neq d,\; \mathrm{perpBisector}(a,b) = \mathrm{perpBisector}(c,d)\}\bigr|.$$
The **rotation energy** counts the ordered congruent quadruples whose difference
vectors are neither equal nor opposite, so it discards the translation and
half-turn channels and isolates the proper-rotation one. A linear map $T$ is
**projection-generic** for a set $G$ when exactly two conditions hold: $T$ sends
the difference of any two distinct points of $G$ to a nonzero vector, and for
two distinct unordered pairs of $G$ the images never combine a parallel pair of
differences with an orthogonal midpoint difference. Perpendicular bisectors,
difference classes and distance images are all `Finset` operations.
## Target
The mission goal is the spherical complete profile: for every finite set $G$
lying on a common sphere, in any dimension, there is a linear map $T$ to the
plane whose image satisfies six conclusions at once —
$$\exists\,T:\quad \mathcal{E}(T(G)) = 2|G|(|G|-1) \;\wedge\; \mathcal{E}(T(G)) \le \mathcal{E}(P') \text{ for every } |P'| = |G| \;\wedge\; \mathrm{rotationEnergy}(T(G)) = 0$$
together with injectivity of $T$ on $G$, general position of the image (no three
collinear, no four cospherical), and exact distance transport. The projection is
chosen per set — its very type depends on the ambient dimension — but a single
projection delivers all six conclusions together, and that bundled form is what
downstream incidence arguments consume.
Milestones ascend in five steps: the universal energy floor, the
bisector-injectivity equality case, the attainment of the floor by
projection-generic maps, the existence of such a map for every
no-three-collinear set, and the no-three-collinear transport bundle that the
goal then specialises to the spherical case.
## Significance
The extremal picture for bisector energy at the level of the exact constant was introduced in Lund–Sheffer–de Zeeuw, and, in footnote 1 on p. 538 of the SoCG 2015 version
(LIPIcs vol. 34, 537–552), state that $\mathcal{E}(P) = 2n(n-1)$ when every
distinct pair determines a distinct bisector, with the enumeration of the
trivial quadruples that proves the floor. The universal asymptotic form
$\mathcal{E}(P) = \Omega(n^2)$ is a remark in their §3.4.
This mission builds a complete machine-checked development of the
floor, its attainment and the sufficiency direction, from first principles in
Lean 4 over mathlib; the `rotationEnergy` statistic together with the
`rotationEnergy = 0` certificate for the projected image, where
`rotationEnergy(P) = 0` follows from the published "distance Sidon set"
property; and a **single** generic projection of a given set that carries the
bisector floor at the same time as the Erdős–Füredi–Pach–Ruzsa general-position
package. Four of that bundle's six conjuncts are already in
Erdős–Füredi–Pach–Ruzsa 1993, whose Theorem 3.1 supplies them.
Formalizing it matters because the argument composes analysis (generic
projections obtained from nonvanishing of circle determinants), algebra
(inner-product and determinant polynomial witnesses carrying
`linear_combination` certificates) and counting (fiberwise difference-class
tallies) — and the interfaces between the three must agree exactly. The
projection-genericity and polynomial-witness lemmas are reusable for any
Euclidean extremal formalization.
## Difficulty
The hard step is keeping the projection generic through every predicate at once:
a projection that preserves no-three-collinearity can still kill a circle
determinant, or create a coincidence that the counting needs to keep distinct.
The naive first idea — project along a random direction and hope — fails because
each predicate forbids a different algebraic hypersurface of directions; the fix
is a single simultaneous-avoidance argument over the union, with each forbidden
set shown proper by an explicit polynomial witness. That step is the largest
proof in the mission and carries its own milestone.
## Formalization scope
Points are `EuclideanSpace`; finite sets are `Finset`; energies are `ℕ`-valued
statistics. Generic projections are linear maps carrying the explicit
two-clause `ProjectionGeneric` predicate, so there is no hidden regularity
assumption. Dimension is a general `ι` with `[Fintype ι]` wherever the transport
needs it. The goal's only hypothesis is membership of a common sphere;
no-three-collinearity is derived from it rather than assumed, because a line
meets a sphere at most twice. No statement is vacuous: explicit witnesses were
checked in the kernel for the goal and for every milestone.
Welcome contributions: the converse of the equality case — bisector injectivity
is proved here to be sufficient for the floor, and necessity is open in this
development; sharpness examples beyond the Erdős–Füredi–Pach–Ruzsa
configuration; and the incidence assembly that consumes this mission's output.
## Selected references
- B. Lund, A. Sheffer and F. de Zeeuw, Bisector energy and few distinct
distances, Proc. 31st SoCG 2015, LIPIcs vol. 34, 537–552, DOI
[10.4230/LIPIcs.SOCG.2015.537](https://doi.org/10.4230/LIPIcs.SOCG.2015.537);
journal version *Discrete Comput. Geom.* **56** (2016), no. 2, 337–356,
DOI 10.1007/s00454-016-9783-5,
[arXiv:1411.6868](https://arxiv.org/abs/1411.6868). Source of the
bisector-energy statistic and its upper bounds. Footnote 1 on p. 538 of the
SoCG version gives $\mathcal{E}(P) = 2n(n-1)$ for every set whose pairs have
distinct bisectors, with the count of trivial quadruples that proves the
floor; §3.4 (p. 545) gives $\mathcal{E}(P) = \Omega(n^2)$ for every set. The
footnote is not in arXiv:1411.6868v1.
- P. Erdős, Z. Füredi, J. Pach and I. Z. Ruzsa, The grid revisited,
*Discrete Math.* **111** (1993), 189–196,
DOI 10.1016/0012-365X(93)90155-M — the lattice-sphere-slice configuration
that gives this mission its name, and (proof of Theorem 3.1, p. 193) the
generic planar projection that is injective, keeps general position and
transports distances.
- J. Solymosi and T. Tao, An incidence theorem in higher dimensions,
*Discrete Comput. Geom.* **48** (2012), no. 2, 255–280,
DOI 10.1007/s00454-012-9420-x,
[arXiv:1103.2926](https://arxiv.org/abs/1103.2926), §5.1 — the canonical
statement of the generic-projection trick this construction borrows. The same
trick is used in J. Pach and F. de Zeeuw, Distinct distances on algebraic
curves in the plane, *Combin. Probab. Comput.* **26** (2017), no. 1, 99–117,
[arXiv:1308.0177](https://arxiv.org/abs/1308.0177).
- McKenna, Lean formalization (mathlib-only, axiom-clean),
[lean-formalizations](https://github.com/mysticflounder/lean-formalizations),
module `Geometry.Euclidean.NearEnemyTheorem`.
20 thms1 active userReviewed
🏆Completed
Captain: mysticflounder
Pach-de Zeeuw: finite Bezout bound for real plane curvesResearch Paper
## Motivation
The **distinct-distances problem** asks how few distinct distances a finite planar
point set can determine. Guth and Katz proved the near-optimal bound
$\Omega(n / \log n)$ in 2015. Their argument passes through incidence geometry:
distances become incidences between points and curves, and the Elekes–Sharir
framework converts the problem into an incidence bound for lines in
three-space. Pach and de Zeeuw showed the same pipeline works for points on a
fixed algebraic curve, replacing line incidences with curve incidences. The
algebraic prerequisite for that replacement — that two bounded-degree real
plane curves with no shared component meet in finitely many points, with an
explicit degree-dependent bound — is what this mission formalizes.
## Setting
A **real plane curve** here is the real zero set of a nonzero bivariate polynomial
$p \in \mathbb{R}[x, y]$, written $V(p) = \{(x,y) : p(x,y) = 0\}$. Its
**total degree** is the maximum $i+j$ over monomials $x^i y^j$ with nonzero
coefficient. A curve is **irreducible** when its polynomial is irreducible.
The paper says two curves have a **common component** when their polynomials
share a nonconstant factor. The Lean development uses a different, weaker
hypothesis, `NoCommonCurveComponent`: no *infinite* irreducible real curve lies
inside both sets. A shared factor whose real zero set is finite (for example
$x^2 + y^2$) violates the paper's hypothesis but satisfies the Lean one, so the
Lean theorem covers strictly more pairs of curves than the paper's statement.
**Currying** views $p$ as a univariate polynomial in one coordinate whose
coefficients are polynomials in the other. In the Lean code the polynomial
variable is coordinate $0$ and the coefficient (base) variable is coordinate $1$;
this description writes the base coordinate as $x$ and the fiber coordinate as
$y$, so a line $\{x = c\}$ is called **vertical**. The **resultant** of two
curried polynomials is a polynomial in $x$ alone. The development uses one
direction of its defining property: if the two specializations at $x$ share a
real root, the resultant vanishes at $x$. All Lean statements use
`MvPolynomial (Fin 2) ℝ` for plane polynomials and `EuclideanSpace ℝ (Fin 2)`
for points.
## Target
The mission's goal is a finite-intersection bound in the spirit of Theorem 2.1
of Pach–de Zeeuw (Bézout's inequality), but it is not that theorem. It differs
in both directions:
$$ \forall d_1, d_2,\ \exists C > 0,\ \forall C_1, C_2 \text{ of total degree} \le d_1, d_2 \text{ with no common infinite irreducible component}:\quad C_1 \cap C_2 \text{ is finite and } |C_1 \cap C_2| \le C. $$
- The conclusion is an existential degree-dependent constant. The proof's
witness is $C = (d_1+d_2+1)^8 + 1$. The paper's sharp bound $d_1 \cdot d_2$ is
not proved here.
- The hypothesis is the weaker "no common infinite irreducible component"
described above, so the statement is not a formal consequence of the paper's
Theorem 2.1; the shared-finite-factor case is handled separately in the proof
by a singular-point count.
The six milestones are the algebraic inputs: coefficient-root counting, the two
resultant-nonvanishing criteria, the fiber bound, and the two mixed
vertical/nonvertical pair bounds that carry the constant $d_1 \cdot d_2$. The
nonvertical–nonvertical pair bound (`primitive_nonvertical_pair_intersection_bound`)
carries the cruder constant $((d_1+d_2)^2+1)\cdot\max(d_1,d_2)$. Above the
milestones sit the irreducible-pair assembly with constant $(d_1+d_2+1)^4$ and
the factorized assembly with constant $(d_1+d_2+1)^8$, from which the goal
follows.
## Significance
The result is the algebraic input to the Pach–de Zeeuw distinct-distances
theorem for points on curves: without a uniform finite-intersection bound, the
incidence count that drives the distance bound cannot even be stated. The
formalization pins down every constant and every non-degeneracy hypothesis
(non-verticality, no shared infinite component, coprimality) that the argument
consumes.
The proof composes four toolkits — univariate root counting, Sylvester-matrix
resultant degree bounds, normalized-factor decompositions, and a smooth
implicit-function nonsingularity argument — whose interfaces must agree
exactly. The resulting lemmas (resultant criteria, fiber bounds,
partial-derivative degree bounds) are reusable for other real-algebraic
incidence formalizations over `MvPolynomial`.
## Difficulty
The central difficulty is elimination with explicit constants: the resultant
converts a two-variable intersection problem into a one-variable root count,
but every step (currying, specialization, factor-pair summation) must preserve
a usable degree bound, and the degenerate configurations (vertical fibers,
shared factors with finite real zero set, singular points) each need a separate
finite bound.
The textbook route — Bézout's inequality over $\mathbb{C}$, then observing
that real intersection points are complex ones — is not taken, for two
reasons. Mathlib has no plane-curve Bézout theorem to invoke. And under the
weaker Lean hypothesis the two polynomials may share an irreducible factor with
finite real zero set, in which case the complex intersection is infinite and no
complex count applies; that branch is closed by bounding the singular points of
the shared factor instead.
## Formalization scope
Points are `EuclideanSpace ℝ (Fin 2)`; curves are `MvPolynomial (Fin 2) ℝ`
zero sets; finiteness is `Set.Finite` with `Set.ncard` bounds. The development
commits to total degree (not weighted degrees) and to the currying order that
eliminates Lean coordinate $0$; `variable`-style implicit degree bounds
$d_1, d_2$ are explicit `{d₁ d₂ : ℕ}` binders on the platform. No statement is
vacuous: every intersection bound carries the non-degeneracy hypothesis
(non-associated irreducibles, non-divisibility, nonzero partials) that excludes
the infinite-intersection cases. Contributions welcome: the sharp $d_1 d_2$
general bound (currently an existential constant), the paper's hypothesis form
(no common factor at all), and the incidence assembly that consumes this
mission's output.
## Selected references
- János Pach and Frank de Zeeuw, Distinct distances on algebraic curves in the
plane, Combin. Probab. Comput. 26 (2017), no. 1, 99–117,
[arXiv:1308.0177](https://arxiv.org/abs/1308.0177), DOI
10.1017/S0963548316000225. Theorem 2.1 there cites C. G. Gibson, Elementary
Geometry of Algebraic Curves, Lemma 14.4, for Bézout's inequality.
- McKenna, Lean formalization of the algebraic preliminaries and Bézout bound,
[lean-formalizations](https://github.com/mysticflounder/lean-formalizations),
modules `PachDeZeeuw.AlgebraicPrelim` and `PachDeZeeuw.Bezout` (mathlib-only,
axiom-clean).
39 thms1 active userReviewed
Captain: mysticflounder
Superlinear or exact bounds for planar distinct distancesOpen Problem
# Superlinear or exact bounds for planar distinct distances
## Motivation
This mission asks how restrictions on collinear and cocircular points limit
the reuse of distances in the plane. Its central question is
[Erdős Problem 98](https://www.erdosproblems.com/98): must the minimum number
of distances grow faster than the number of points?
## Setting
For each positive integer n, let h(n) be the minimum number of distinct
positive Euclidean distances determined by an n-point set in the plane with
no three collinear points and no four cocircular points. Write D(P) for the
number of distinct positive Euclidean distances determined by P.
## Target
The mission is to establish a superlinear lower bound, or determine this
extremal function exactly. The superlinear target is Erdős Problem 98:
$$\lim_{n\to\infty} h(n)/n=\infty.$$
Concretely, for every real A > 0, prove that there is an integer n_A such
that every general-position configuration P with |P| = n >= n_A satisfies
D(P) > A n. A fixed improvement of the coefficient 1/3, or an additive
sublinear improvement above n/3, does not complete this objective.
The alternative completion target is an exact determination of h(n), proved
by a universal lower bound and general-position constructions attaining that
bound. State the range of n explicitly. An asymptotic estimate or a
counterexample to superlinearity alone must be labeled with its actual scope;
neither is an exact determination of h(n).
## Significance and supporting results
The current strongest internally audited
[prose result in this project](https://github.com/flound1129/esgk-on3/blob/main/docs/results/esgk-n14-atomic-proof-2026-09-13.md) is
$$D(P)\ge n/3+c n^{1/4}$$
for some absolute c > 0 and all sufficiently large n. Its full Lean
formalization remains open. The n^(1/4), n^(1/5), and n^(1/6) theorem targets
and their existing milestones are supporting results, not the mission's
terminal goal. Resolving the superlinear target would establish a lower bound
above every fixed linear coefficient. Determining h(n) exactly would settle
the corresponding extremal problem with matching constructions.
## Difficulty and research priorities
The n^(1/4) route constructs a deficiency--Newton carrier, proves pair
separation, and applies one polynomial partition to obtain the curve bound
D(S) >= c d^(-4/3) |S|^(4/3). Its current final calculation yields an additive
n^(1/4) term. Stronger additive bounds count as intermediate progress; they
must not be reported as a superlinear lower bound.
- Develop an argument that excludes D(P) <= A n for every fixed A > 0.
The repository's fixed-A distance-energy gap is one sufficient route.
- Investigate additional structure of the Newton carriers and interactions
between their factors, or another geometric or combinatorial route that
can control the superlinear target.
- Investigate constructions and universal lower bounds together when
pursuing an exact extremal determination.
- Preserve and formalize useful intermediate theorems while keeping their
statements and remaining premises explicit.
## Formalization scope
Configurations are finite subsets of the Euclidean plane, represented in the
project by injective maps from `Fin n` to the plane. Both general-position
hypotheses apply to the image. D(P) counts distinct positive distance values,
not pairs or ordered multiplicities. The superlinear quantifier ranges over
every real A > 0 and every sufficiently large general-position configuration.
The superlinear target and exact-determination target remain open here.
Distinguish conjectures, conditional reductions, audited prose proofs, and
kernel-checked Lean results. A completed supporting formalization does not
by itself complete this mission.
## Selected references
- [Erdős Problem 98](https://www.erdosproblems.com/98) — extremal question and
bibliography.
- [Project overview](https://github.com/flound1129/esgk-on3/blob/main/README.md)
— fixed-A target and current theorem status.
- [Atomic proof of the ESGK n^(1/4) additive bound](https://github.com/flound1129/esgk-on3/blob/main/docs/results/esgk-n14-atomic-proof-2026-09-13.md),
project manuscript, revised 2026-09-14.
- [Full-proof audit](https://github.com/flound1129/esgk-on3/blob/main/docs/audits/esgk-n14-strengthened-full-audit-2026-09-14.md),
internal adversarial review, 2026-09-14.
11 thms2 active users
Captain: xuanji
Circle packing in a square: exact constantsTextbook
## Motivation
Packing congruent circles into a square is a classical problem in discrete geometry: for each natural number $n$, choose a common radius as large as possible while keeping all disks inside the square and preventing overlap. Every exact value requires two logically distinct achievements: an explicit configuration attaining the proposed radius and a proof that no configuration can do better.
The character of those proofs changes sharply with $n$. The first cases admit short geometric arguments; later cases use contact-graph analysis, specialized case divisions, or computer-assisted global optimization with interval arithmetic. Formalizing the resulting constants therefore provides a growing benchmark for extremal geometry, real algebra, finite configurations, and verified computation in Lean.
This is an **open-ended formalization mission**. It begins with the exact constants currently represented by theorem-backed milestones, but it is not restricted to a fixed terminal value of $n$. Further milestones may be added whenever an exact packing value and its rigorous optimality argument are identified and stated precisely enough for formalization.
## Setting
A point is a pair of real coordinates. For points $p=(x,y)$ and $q=(x',y')$, squared Euclidean distance is
$$
\operatorname{sqDist}(p,q)=(x-x')^2+(y-y')^2.
$$
For a real radius $r$, a point lies in the inner square when both coordinates belong to the closed interval $[r,1-r]$. This is exactly the coordinate condition saying that a closed disk of radius $r$, centered at that point, is contained in the unit square.
The predicate $\operatorname{Packable}(n,r)$ requires $0\le r\le \tfrac12$ and a family of $n$ centers in the inner square such that the squared distance between every two distinctly indexed centers is at least $(2r)^2$. Equality is allowed, so tangent disks are admitted. Radius zero is also admitted.
Define
$$
r_n=\sup\{r\in\mathbb R:\operatorname{Packable}(n,r)\}
$$
and define the optimal covered-area fraction by
$$
c_n=n\pi r_n^2.
$$
It is often convenient to use the equivalent point-separation constant $d_n$, the greatest possible minimum pairwise distance among $n$ points in the unit square. The conversion is
$$
r_n=\frac{d_n}{2(1+d_n)},
\qquad
c_n=n\pi\left(\frac{d_n}{2(1+d_n)}\right)^2.
$$
The Lean definitions use a supremum rather than assuming in advance that an optimal packing is attained.
## Current exact-value milestones
The mission currently contains theorem-backed milestones for the following values:
| $n$ | Exact separation or area value | Proof character in the supplied notes |
|---:|---|---|
| $2$ | $d_2=\sqrt2$, hence $c_2=\pi(3-2\sqrt2)$ | diagonal bound |
| $3$ | $d_3=\sqrt6-\sqrt2$ | minimum enclosing square of a triangle |
| $4$ | $d_4=1$, hence $c_4=\pi/4$ | convex hull and perimeter |
| $5$ | $d_5=1/\sqrt2$ | four-cell pigeonhole argument |
| $6$ | $d_6=\sqrt{13}/6$ | case-specific geometric proof |
| $7$ | $d_7=4-2\sqrt3$ | hand proof and later computer verification |
| $8$ | $d_8=\sqrt{2-\sqrt3}$ | case-specific geometric proof |
| $9$ | $d_9=1/2$, hence $c_9=\pi/4$ | classical geometric proof |
| $16$ | $d_{16}=1/3$, hence $c_{16}=\pi/4$ | theoretical grid-optimality proof |
| $25$ | $d_{25}=1/4$, hence $c_{25}=\pi/4$ | theoretical grid-optimality proof |
| $36$ | $d_{36}=1/5$, hence $c_{36}=\pi/4$ | theoretical grid-optimality proof |
For rows stated using $d_n$, the corresponding milestone for $c_n$ uses the conversion formula above. The equalities are claims about the supremum-defined packing constants, not merely about the displayed candidate configurations.
## An extensible mission
The milestone list is intended to grow. The supplied survey notes classify $n=2,\ldots,33$ and $n=36$ as rigorously solved in the cited literature, while distinguishing $n=34$ and $n=35$ as not rigorously closed in the cited 2021 account. Many of the computer-assisted cases do not have a simple radical expression in the supplied notes. Before such a case is linked to a Lean theorem, its primary source must provide a precise candidate value, algebraic characterization, certified enclosure, or optimal-configuration certificate that can be stated faithfully.
A new milestone should identify:
1. the precise value or exact characterization being formalized;
2. an attaining configuration or a certified existence argument;
3. a universal upper bound or global-optimality certificate;
4. the primary source and exact theorem, equation, or certificate location;
5. any trusted computational artifact and the arithmetic guarantees it requires.
Numerical evidence and strong bounds are valuable, but they must be labeled as bounds rather than exact-value milestones. Conversely, newly published exact results for larger $n$ may be added without changing the underlying definitions.
## Proof obligations
Every exact-value milestone must connect the proposed value to `Packable`, `r_n`, and `c_n`. Constructing a configuration establishes only a lower bound. An upper-bound argument without attainability also does not establish equality. A complete proof must bridge both directions through the supremum definition.
The proof methods may include:
- elementary diameter, pigeonhole, convexity, or enclosing-shape arguments;
- normalization between disk centers and point-separation configurations;
- contact-graph and boundary-constraint analysis;
- finite case decompositions;
- interval arithmetic and formally checked branch-and-bound certificates;
- exact algebraic identities needed to convert $d_n$ into $r_n$ and $c_n$.
Shortcuts that redefine $r_n$, $d_n$, or $c_n$ to equal a desired answer are excluded. The constants must remain consequences of the common geometric model.
## Mission structure
The root theorem `CirclePackingConstants.c_all` is the conjunction of the eleven exact-value milestones currently in the mission, covering $n=2,3,4,5,6,7,8,9,16,25,36$. Its proof sketch reduces the root directly to those milestone theorems, so the mission remains open until every current exact value is proved.
The milestone theorems remain separately reusable and independently auditable. When further exact values are added, a successor aggregate theorem can extend the conjunction and become the new root without replacing the shared definitions or invalidating earlier results.
This structure allows elementary cases, historical hand proofs, and computer-assisted certificates to progress independently while remaining part of one cumulative library of exact circle-packing constants.
## Formalization scope
The Lean model uses `ℝ × ℝ` for points and an explicit coordinate formula for squared Euclidean distance. Disk containment is represented by inclusive coordinate inequalities. Nonoverlap is represented by a weak squared-distance inequality, so tangency is permitted. The indexing type is `Fin n`, and the definitions apply to every natural number, including zero.
The definition bundle contains only `Point`, `sqDist`, `InInnerSquare`, `Packable`, `r_n`, and `c_n`. Solvers may introduce normalization maps, separation bounds, explicit configurations, supremum lemmas, contact structures, certificate checkers, and radical or polynomial identities as auxiliary declarations.
## Selected references
- User-supplied notes, *Circles in squares: constants, proofs, and what is actually known*, supplied September 12, 2026. The notes summarize the exact small-$n$ formulas, grid cases, historical proof taxonomy, and computer-assisted frontier used to organize this mission.
- J. Schaer and A. Meir, “On a geometric extremum problem,” *Canadian Mathematical Bulletin* 8 (1965), 21–27.
- J. Schaer, “The densest packing of nine circles in a square,” *Canadian Mathematical Bulletin* 8 (1965), 273–277.
- B. L. Schwartz, “Separating points in a square,” *Journal of Recreational Mathematics* 3 (1970), 195–204.
- J. B. M. Melissen, “Densest packing of six equal circles in a square,” *Elemente der Mathematik* 49 (1994), 27–31.
- M. C. Markot, “Improved interval methods for solving circle packing problems in the unit square,” *Journal of Global Optimization* 81 (2021), 773–803.
- Erich Friedman, *Circles in Squares*, Erich's Packing Center, for background tables and diagrams of candidate packings.
32 thms5 active users
Captain: hao jia
Uniform Obstacle Bounds for Planar Graphs (OPG-37357)Open Problem
## Motivation
An obstacle representation turns a graph into a visibility system: vertices are points in the plane, and nonedges are blocked by polygonal obstacles. The **obstacle number** asks for the minimum number of obstacles needed. OPG-37357 records two different questions for planar graphs. The first asks whether one obstacle can ever be insufficient. The second asks whether some universal constant bounds the ordinary obstacle number of every planar graph.
The status of the two parts is different. Berman, Chappell, Faudree, Gimbel, Hartman, and Williams proved in 2017 that explicit planar graphs, including the icosahedron and their graphs $X_4$ and $X_6$, have ordinary obstacle number two. Thus the first question has a published positive answer. The universal-constant question remains the research target here. A separate invariant called planar or plane obstacle number requires a crossing-free visibility drawing; results for that invariant must not be substituted for the ordinary obstacle number used by this mission.
## Setting
A finite simple graph $G$ has a **$k$-obstacle drawing** when its vertices are placed injectively as points in $\mathbb R^2$ and there are $k$ pairwise disjoint closed connected polygonal obstacles such that
$$
uv\in E(G)
\quad\Longleftrightarrow\quad
[p(u),p(v)]\text{ meets no obstacle}.
$$
Graph vertices lie outside every obstacle. The **ordinary obstacle number** $\operatorname{obs}(G)$ is the least such $k$. The drawing itself may contain crossings between visible graph edges; planarity is a property of the abstract input graph, not an extra constraint on the obstacle drawing.
The Lean model represents a polygonal obstacle as a connected finite union of closed filled triangles. This gives a compact polygonal region with exact real-coordinate segment incidence. Straight-line planarity of the abstract graph is represented separately.
## Formalization targets
### The two-part OPG record
The source records both
$$
\exists\text{ finite planar }G,\ \operatorname{obs}(G)>1
$$
and
$$
\exists k\in\mathbb N\ \forall\text{ finite planar }H,
\ \operatorname{obs}(H)\le k.
$$
The first assertion is known in the literature and appears as a published-result milestone. The second is open and is therefore the mission's main theorem. Together they preserve the two-part source without presenting the whole record as unresolved.
### Published first part
A milestone formalizes the stronger published statement
$$
\exists\text{ finite planar }G,
\qquad \operatorname{obs}(G)\le2
\quad\text{and}\quad
\operatorname{obs}(G)\not\le1.
$$
This captures ordinary obstacle number exactly two without hard-coding one graph before its adjacency data and lower-bound certificate are formalized.
### Universal bound
The open milestone asks for a single natural number $k$, chosen before the graph, that works for every finite planar graph. The number of obstacle corners is not bounded by this theorem; only the number of connected polygonal obstacles is.
## Significance
The published first part establishes that planarity alone does not force a one-obstacle representation. The second part asks whether planar graphs nevertheless have uniformly bounded visibility complexity. A positive answer would produce a common finite obstacle budget independent of graph order; a negative answer would require a family of planar graphs with unbounded ordinary obstacle number.
Formalization is especially useful because several nearby notions differ by one word but have different known bounds: ordinary versus plane obstacle number, arbitrary polygonal versus convex obstacles, and fixed-placement versus freely chosen drawings. The mission's definitions make those choices explicit and provide reusable segment-obstacle semantics for later geometric graph formalizations.
## Difficulty
A finite combinatorial graph does not come with a canonical visibility drawing. Even when one starts with an arbitrary connected blocking set, replacing it by one bounded simple polygon requires compactness, component, incidence, and polygonal-neighborhood arguments. Conversely, lower bounds must quantify over every possible placement and obstacle, not merely refute a selected coordinate drawing.
Counting results for unrestricted graphs do not automatically preserve planarity. Bounds for planar obstacle number impose a crossing-free drawing and therefore answer a different question. The known two-obstacle examples close only the existential first part and give no universal $k$.
## Formalization scope
All graph vertex types are finite. Obstacles are closed connected polygonal regions represented by finite triangle unions; they are pairwise disjoint and avoid graph vertices. Visibility uses the full closed segment, so tangency or boundary contact blocks a nonedge. The planarity witness is independent of the obstacle drawing. Empty and one-vertex graphs remain in the universal quantifier and should be handled without division or nonemptiness assumptions.
The repository's fixed-placement polygonization argument and finite arrangement code are `candidate_only`. They may motivate supporting lemmas, but they neither prove the unrestricted obstacle-drawing completeness theorem nor settle the universal bound. Contributions are welcome on exact geometry primitives, the published two-obstacle construction and lower bound, conversions between connected blockers and polygonal obstacles, and the universal root. A proof for the plane invariant, convex invariant, one fixed drawing, or a finite order cutoff must be labeled at that narrower scope.
## Selected references
- L. W. Berman, G. G. Chappell, J. R. Faudree, J. Gimbel, C. Hartman, and G. I. Williams, *Graphs with Obstacle Number Greater than One*, JGAA 21(6), 2017. https://doi.org/10.7155/jgaa.00452
- J. Gimbel, P. Ossona de Mendez, and P. Valtr, *Obstacle Numbers of Planar Graphs*, Graph Drawing 2017. https://arxiv.org/abs/1706.06992
- M. Balko, S. Chaplick, R. Ganian, S. Gupta, M. Hoffmann, P. Valtr, and A. Wolff, *Bounding and Computing Obstacle Numbers of Graphs*, SIAM Journal on Discrete Mathematics 38(2), 2024. https://arxiv.org/abs/2206.15414
- Open Problem Garden / UnsolvedMath, *OPG-37357*. https://www.unsolvedmath.com/problems/OPG-37357
6 thms4 active usersReviewed
Captain: xuanji
230 space groupsTextbook
## Motivation: classify three-dimensional periodic symmetry
A **space group** describes the rigid motions compatible with a periodic spatial symmetry. The classification concerns possible symmetry types, rather than the size or shape of a particular drawing of a crystal. The classical three-dimensional numbers are 230, 219 when mirror-related types are identified, and 65 for the orientation-preserving subfamily. These are the three numbers recorded in [Oliver Knill’s survey, §94, “Crystallography,” p. 41](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Keeping their conventions separate matters: changing which coordinate transformations are allowed changes what counts as the same type.
The target is the known classification result selected by **LeanEval v1**, not an unsolved classification conjecture. Its authoritative specification is [the declaration `LeanEval.Geometry.SpaceGroupsProblem.space_groups`](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The accompanying [benchmark manifest](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml) attributes the classification independently to Fedorov and Schoenflies in 1891. The work requested here is a machine-checked proof of that fixed statement.
## Setting: groups, transformations, and orientation
For a natural number $d$, let $E(d)=\mathbb R^d$ with its Euclidean inner product. A **Euclidean isometry** is an invertible affine distance-preserving transformation of this space. The objects being counted are subgroups $G$ of this full motion group. In the [benchmark’s definitions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), $G$ is **discrete** when, for every point $x$ and every real $\varepsilon>0$, the set of its elements satisfying $\operatorname{dist}(gx,x)\leq\varepsilon$ is finite.
Such a group is **crystallographic** when it also contains translations by the members of some linearly independent family of $d$ vectors. Translation by $v$ means exactly that the transformation sends every $x$ to $x+v$. These conditions specify the underlying groups directly; they do not start with a list of previously classified examples. Although the structure field containing the translation condition is called `cocompact`, its actual content is the existence of these independent translations, not a separately assumed compact quotient.
An **affine equivalence** between two groups is an invertible affine map whose conjugation carries the first group’s set of transformations onto the second’s. It need not be an isometry. An **orientation-preserving affine equivalence** additionally requires the determinant of that affine map’s linear part to be positive. Separately, an individual isometry preserves orientation when its own linear part has positive determinant. The **Sohncke subfamily** restricts the groups themselves: every element of a group must preserve orientation. This is distinct from restricting the map used to compare two groups, as explicitly distinguished by the [source definitions and notes](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean).
## Target: one conjunction, with all three exact counts
Write $C_{\mathrm{OP}}(d)$ for `crystallographicCountOP d`, $C(d)$ for `crystallographicCount d`, and $C_{\mathrm{OP,only}}(d)$ for `crystallographicCountOPOnly d`. They count, respectively, orientation-preserving affine classes of all crystallographic groups, arbitrary affine classes of all crystallographic groups, and orientation-preserving affine classes within the all-elements-orientation-preserving subfamily. The sole goal is
$$
C_{\mathrm{OP}}(3)=230\quad\land\quad C(3)=219\quad\land\quad C_{\mathrm{OP,only}}(3)=65.
$$
This is the [exact benchmark conjunction](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), in its original order. None of its three components is optional, and they are not separate theorem targets. There are no milestones or auxiliary theorem items.
## Significance: exact cardinalities for the underlying groups
The result gives finite and exact answers for the specified spaces of symmetry types, while retaining the distinction between orientation of a coordinate change and orientation of every symmetry in a group. The difference between 230 and 219 reflects the identification of mirror-related types described in [Knill, §94](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf); the 65 count answers a different question, concerning the restricted subfamily. Neither a single count nor a list that silently merges the equivalence conventions establishes the full assertion.
The formalization would add a proof connecting these numerical claims to the actual groups and class subsets specified in Lean. The [benchmark source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) currently supplies the statement with an unproved placeholder. This draft likewise supplies a statement, not a proof or a claim that the benchmark is solved.
## Difficulty: a catalog is not a completeness theorem
A finite catalog can have 230 entries without representing every crystallographic group, and different entries can still represent the same affine class. Thus checking the length of a catalog alone does not establish the [source’s cardinality assertion](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The difficulty is the mathematical connection between concrete descriptions and all groups admitted by the definitions, with precisely the required equivalence relations. The restricted 65-count must also respect the condition on every group element, rather than just a label attached to an example.
## Formalization scope: preserve the benchmark model
The Lean representation is `EuclideanSpace ℝ (Fin d)`, with affine isometries and affine equivalences from Mathlib. The [three source counting functions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) use `Set.encard` in the extended natural numbers $\mathbb N\cup\{\infty\}$. More precisely, each counts the set of subsets obtained as the class of some admissible group; it does not count representatives with multiplicity. Consequently, the displayed finite equalities include finiteness, which is not assumed beforehand.
One reusable definition bundle contains exactly the source’s model spaces, translation and discreteness predicates, crystallographic-group subtype, orientation predicate, two conjugacy relations, and three counting functions. Their declarations are preserved, including definitions for every natural dimension; only the theorem fixes $d=3$. Definitions for group actions, affine conjugation, and these class subsets can be used independently of this particular count. Contributions must establish the fixed goal with these meanings. Replacing the groups by a hard-coded finite type, defining a count to be its desired answer, or importing an unproved classification into the definition bundle would not establish this target.
## Selected references
- LeanEval contributors; problem submitted by Kim Morrison. *LeanEval v1: 230 space groups*, statement revision 1, 2026, repository commit `296b7491ec989d21bcf8636a9a69231a1e5d1d25`. [Exact Lean source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean); [manifest with historical bibliography](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml).
- Oliver Knill. *Some Fundamental Theorems in Mathematics*, author-hosted expository survey, July 22, 2018; updated June 25, 2023. §94, “Crystallography,” p. 41. [Full text](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). This provides background for the three counts; the exact formal conventions are those of LeanEval above.
6 thms2 active usersReviewed
🏆Completed
Captain: mysticflounder
Erdős Problems 97 and 96: Convex Point Sets and Unit DistancesOpen Problem
# Closed — negative resolution of Erdős Problems 96 and 97
Adam McKenna closed this mission on 13 September 2026 following **Unit distances in convex polygons**, by **Liam Kruer, Jensen Kohlmeyer, and Liam Price**. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.
[Paper and complete Lean source](https://github.com/Leeham06972452/erdos-96-97/tree/0e98f5f9bdaf36007e3eb405cbefe2eda778a9b2). All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.
**Do not start further proof attempts or solver runs for the affirmative conjectures.** Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.
---
## Historical mission description
# Motivation
The mission is to prove the combined open goal
$$
\text{Problem 97} \;\land\; \text{Problem 96}
$$
for finite point sets in strictly convex position in the Euclidean plane.
## Why Problems 97 and 96 belong together
Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every
nonempty convex-independent finite set then has a vertex with at most three
neighbors at each positive radius, in particular at radius $1$. Delete that
vertex and preserve convex independence. Apply the same step to every subset
created by deletion until no points remain.
Charge each unordered unit-distance pair to the first endpoint deleted. Each
deleted vertex receives at most three charges, so an $n$-point set determines
at most $3n$ unordered unit-distance pairs. This gives the Problem 96 bound
and therefore $O(n)$. The package uses this one-way dependency; it does not
seek a reverse implication.
# Setting
Let $A\subset\mathbb R^2$ be finite. Strict convex position means that every
point of $A$ is an extreme point of the convex hull of $A$. For $p\in A$, the pinned
multiplicity at radius $r>0$ counts points $q\in A$ with
$\lVert p-q\rVert=r$. Problem 97 asks for a point where no radius has four
such other points. Problem 96 counts unordered pairs at distance $1$, then
takes the supremum over convex-independent $n$-point sets.
The historical progression is part of the setting. Erdős’s 1946 paper posed an
earlier three-neighbor version. His 1987 account reports Danzer’s convex
nonagon in which every vertex has three equidistant witnesses, and asks about
four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex
configuration with the same unit distance at every vertex, placing the local
question beside the unit-distance problem.
# Target
The Problem 97 target is the canonical statement that every nonempty finite
convex-independent $A$ has no four-equidistant-point property:
$$
\forall A,\quad A\ne\varnothing\;\to\;\operatorname{ConvexIndep}(A)
\;\to\;\neg\operatorname{HasNEquidistantProperty}(4,A).
$$
The Problem 96 target is the canonical asymptotic statement
$$
U_c(n)=O(n),
$$
where $U_c(n)$ is the supremum of the unordered unit-distance counts
determined by convex-independent $n$-point sets. The bound is asymptotic;
the Problem 97 route would give the stronger explicit bound $U_c(n)\le3n$
for every natural number $n$.
# Significance
The package records a formal proof route joining a pinned geometric obstruction
to a global extremal bound. A successful Problem 97 proof would immediately
settle Problem 96 with the explicit constant $3$, while preserving the
combinatorial meaning of the count. It also separates the historical
three-neighbor constructions from the still-open four-neighbor assertion.
# Difficulty
The source proof reduces Problem 97 to strong induction on $|A|$. Its counting
engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness
refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib
(2013). This engine forces every counterexample to have at least nine points; a
finite geometric analysis excludes exactly nine points; and the remaining step must
produce a removable vertex for every larger minimal counterexample. The
removable-vertex statement carries the induction hypothesis that every
strictly smaller nonempty convex 4-equidistant set is contradictory. That
large-cardinality geometric step remains open, so both headline targets remain
open. Finite computational certificates can support local cases but do not
replace the universal geometric statement.
# Counterexample routes
Problem 97 is open, so the mission also records the parallel negative route.
The source formalization calls a nonempty convex-independent
finite set with the four-equidistant property a
[`Problem97.IsCounterexample`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/a46894f6078319d3001d06310531df50af0f6bbd/lean/Erdos9796Proof/P97/UniversalProblem97.lean#L24-L29).
Constructing one such set would refute Problem 97 and therefore refute the
mission's affirmative conjunction, regardless of whether Problem 96 remains
true. The counterexample milestone keeps this resolution path visible beside
the nonexistence proof. A successful witness must use exact coordinates or
exact algebraic data from which Lean verifies both strict convex position and
the four-equidistant property; a numerical approximation or a realizable
incidence pattern alone is insufficient.
Problem 96 has its own negative route. Because its claim is asymptotic, one
finite convex configuration cannot refute it. A counterexample must instead
give convex-independent point sets at arbitrarily large cardinalities whose
unit-distance counts exceed every proposed linear constant. The mission tracks
this superlinear-family statement separately, together with a reduction from
it to the exact negation of Problem 96. This keeps both possible outcomes
visible: a direct or Problem-97-derived linear upper bound, and an explicit
family proving that no such bound exists.
# Formalization scope
The canonical source is pinned at commit
`757d852766f377f7c1a0ffeeef6d3526bc0cb7a4`. It contains the formal source
statements for [Problem 97](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/UpstreamBridge.lean#L30)
and [Problem 96](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P96/UpstreamBridge.lean#L96).
The source repository reports closed proofs of the conditional bridge to the $3n$ bound
([conditional three-times bound](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P96/EuclideanPeeling.lean#L273)),
the $|A|\ge9$ counting milestone
([nine-point counting bound](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/Counting.lean#L95)),
and the exact nine-point exclusion
([exact nine-point exclusion theorem](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/N9Endpoint/Closure.lean#L56)).
The remaining large-cardinality milestone is the
[removable-vertex step](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/RemovableVertexAxiom/RemovableVertexOfLarge.lean#L50),
with its minimality hypothesis retained. The current platform mission contains
accepted transfers of the counting argument, the conditional bridge, and the
exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make
convex independence and the positive-radius condition explicit; no theorem is
assumed inside a definition. Singletons and two-point sets are included in
Problem 97, while Problem 96's counting definitions also include the empty set.
The source repository uses Lean `v4.27.0`; these mission statements target the
platform's `v4.33.1`. Source-proof transfer and revalidation remain separate work.
The Lean declarations and proofs are this project's own formalization. The
Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical
provenance; they do not indicate that a paper proof was imported or
machine-checked directly.
These source results establish the intended dependency graph: the P97 universal
root feeds low-unit-degree extraction, strong induction, and then the P96
supremum bound. The platform mission records those contracts and milestones;
it does not claim to have transplanted their proof bodies.
The milestones include the two canonical roots, their conditional bridge, the
`|A| ≥ 9` count, the `n = 9` exclusion, the `|A| > 9` removable-vertex step,
the documented Danzer nine-point three-neighbor example, the parallel goal of
constructing a Problem 97 counterexample, and the superlinear-family route to
a counterexample to Problem 96.
# References
- Erdős, *On Sets of Distances of n Points* (1946), [DOI](https://doi.org/10.1080/00029890.1946.11991674).
- Erdős, *Some Combinatorial and Metric Problems in Geometry* (1987), [scan](https://www.renyi.hu/~p_erdos/1987-27.pdf).
- Fishburn–Reeds, *Unit Distances Between Vertices of a Convex Polygon* (1992), [publisher record](https://www.sciencedirect.com/science/article/pii/092577219290026O).
- Dumitrescu, *On Distinct Distances from a Vertex of a Convex Polygon* (2006), [Springer record](https://link.springer.com/article/10.1007/s00454-006-1262-y); provenance for the source counting method.
- Nivasch–Pach–Pinchasi–Zerbib, *The Number of Distinct Distances from a Vertex of a Convex Polygon* (2013), [arXiv:1207.1266](https://arxiv.org/abs/1207.1266); provenance for the cap-witness refinements used by the source formalization.