Erdős Problem 1207

Read formalization.yaml

method

autonomous — GPT-6 Astra (pre-release version, OpenAI)

review

other — kernel-checked by lean 4 v4.27.0 when this repository builds, with an in-repo audit (audit.lean and scripts/audit.sh) confirming that challenge.lean and solution.lean give the theorem the same fully explicit type and that it depends only on propext, quot.sound and classical.choice. the external comparator and its independent nanoda replay could not be run, because no comparator or lean4export release supports this repository's pinned lean v4.27.0. no human has refereed the argument; no informal review and no independent refereeing.

sorry

0 unproved goals declared

sources

Proof of Erdős problem #1207: there is c > 0 with P_2(n) < n^(1-c) for all sufficiently large n, where P_2(n) is the least, over n-point planar sets, of the largest isosceles-free subset. — other; Erdős problem #1207 (erdosproblems.com) — background; A survey of problems in combinatorial number theory — background; Isosceles triangles determined by a planar point set — background

related

epoch-research/LeanOpenProblems/blob/8fa3b4c6ee5e6f0ee25d027b6f110f20787db977/apn/data/erdos_autoformalized/Isolated/Erdos1207.erdos_1207.lean — builds-on

divergences

Relative to the erdosproblems.com statement there is no known divergence. P d n is the infimum over n-element finsets of EuclideanSpace ℝ (Fin d) of the supremum of cardinalities of isosceles-free subsets of that finset, which is exactly P_d(n): for every n such a finset exists, and the inner set of cardinalities is nonempty and bounded by n, so neither sInf nor sSup takes its junk value 0. A set is isosceles-free when no three distinct points have two equal distances among them (IsIsosceles p q r is dist p q = dist q r or dist q r = dist r p or dist r p = dist p q, so degenerate collinear isosceles triples count, matching the problem's remark that the case d = 1 is the three-term-progression problem). The conclusion reads "for some constant c > 0 and all sufficiently large n" with the real power n^(1-c); the informal question does not specify the range of n, and any c at most 1 forces P_2(n) at least 2 for n at least 2, so the eventual quantifier is the natural reading. The value of c is existential and not advertised.

checked by

nobody independent of its authors yet