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.