we-solve (beta)

Math-536 · mathematics · Geometry

Small Triangles in the Unit Disc

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
Unless a section says otherwise, ${\mathbb{N}}=\{1,2,\ldots\}$, ${\mathbb{Z}}$ is the ring of integers, ${\mathbb{Q}},{\mathbb{R}},{\mathbb{C}}$ are the rational, real, and complex fields, $[N]=\{1,\ldots,\lfloor N\rfloor\}$, and $\log$ is the natural logarithm. For real functions of a parameter tending to infinity, $f\ll g$ and $f=O(g)$ mean $|f|\leq Cg$ eventually for some fixed $C$; $f\gg g$ reverses this comparison; $f=o(g)$ means $f/g\to0$; $f\sim g$ means $f/g\to1$; and $f\asymp g$ means both order bounds. A subscript on $O$ or $\ll$ specifies allowed constant dependence. The expression $n^{o(1)}$ in an upper bound means growth smaller than $n^\epsilon$ for each fixed $\epsilon>0$. Local definitions govern any exception, finite-field convention, or use of the same symbol for another object. An asymptotic claim is not automatically an effective algorithm.

Use the closed unit disc in ${\mathbb{R}}^2$ and distinct points. For a triple $x,y,z$, its area is $\tfrac12|\det(y-x,z-x)|$, which is zero for collinear triples. If $\Delta(n)$ is the supremum, over $n$-point sets, of their smallest triangle area, the requested upper bound is $\Delta(n)\leq n^{-2+o(1)}$; equivalently, for every $\varepsilon>0$, eventually $\Delta(n)\leq n^{-2+\varepsilon}$. [S1] [S2]

Statement recorded in the supplied source.
Given $n$ points in the unit disc, must there be a triangle of area at most $n^{-2+o(1)}$ determined by them? [S1]
Residual task reported by the archive.

The embedded review (2026-08-17) records: Approach or attain the exponent -2. [S1]

Short English statement

Must every large collection of points in a unit disc contain a triangle whose area is at most an almost inverse-square function of the number of points?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-536-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-536

Heilbronn triangle power improvement: Rescale the unit-square construction into the unit disk.

The claimed counterexample lies within the question’s hypotheses and contradicts its universal conclusion.

Small Triangles in the Unit Disc

OpenAI's claim

Heilbronn triangle power improvement: For every sufficiently large $n$, the paper claims $n$ points in the unit square with every triangle area at least $c n^{-2+\eta}$ for fixed positive $c,\eta$. This contradicts an upper bound with exponent arbitrarily close to minus two.

Mathematical statement of the claimed result

Mathematical claim 1.
For $n\ge3$, define $\Delta(n)=\max_{P\subset[0,1]^2,\ |P|=n}\min_{\{p,q,r\}\subset P}\tfrac12|\det(q-p,r-p)|$. The claim gives absolute $\eta,c>0,n_0$ with \[\Delta(n)\ge cn^{-2+\eta}\quad(n\ge n_0).\] It therefore refutes the proposed upper estimate $\Delta(n)=O_\epsilon(n^{-2+\epsilon})$ for every $\epsilon>0$, by taking $\epsilon<\eta$. A fixed affine scaling transfers the construction to a unit disk.

Outline of the argument

Heilbronn triangle power improvement: Two congruence conditions govern randomly sampled integer columns. Norm-polynomial residues control small nonzero determinants, while an independent quadratic-surface condition and lattice counts handle zero determinants. The Chinese remainder construction combines them, repeated labels supply a deletion saving, and scaling transfers the retained determinant lower bound to triangle areas.

Formal verification

Family 191 describes Lean coverage for the triangle-area improvement along an unbounded sequence of sizes; the every-large-size extension is broader.

Heilbronn triangle power improvement: The manuscript links HeilbronnTriangle.lean.

The documented selection does not cover the entire manuscript assertion relevant here.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →