2026-07-21 08:52 UTCgpt-5.6-sol · high

Mandatory authoritative-source and methods audit followed by an exact semantic discriminator on the Harborth-Fishburn H8 configuration

Progress

The baseline review is complete. The maintained source, original 1975 paper, current and historical formalizations, few-distance classifications, convex-position refinements, and recent citation trails were audited. H8 passed exact checks in 0.043 seconds with peak child memory 17,920 KB. This closes the statement ambiguity but supplies no counterexample to the open global assertion. The next bounded junction is the unique 12-point five-distance configuration.

Strategy and discriminator

counterexample and witness search

Separate global and local distance counts, represent coordinates in Z[sqrt(3)], test every triple determinant and pairwise squared distance exactly, and use few-distance classifications only after checking collinearity.

Hypothesis: The pinned H8 coordinates have no collinear triple, exactly three nonzero distances from each point, and exactly four global distances, so they refute only the local strengthening.

Test: Run the dependency-free exact checker under the experiment recorder and require all 56 triple determinants to be nonzero, all eight local counts to equal 3, and the global count to equal 4.

Rationale

The exact calculation separates the two bundled claims: 3 < floor(8/2) locally, while the four global distances equal floor(8/2). The source audit independently confirms that the maintained open status applies to the global claim and that the local claim is already false.

Claims requiring scrutiny

Erdős problem 1082(i), the global floor(n/2) assertion, remains listed open/falsifiable as of the official page last edited 2026-04-11.
The single-source strengthening 1082(ii) is false.
The explicit H8 configuration has no collinear triple, local distance-count vector [3,3,3,3,3,3,3,3], and four global distances.
Szemerédi's double count proves the general-position lower bound ceil((n-1)/3), locally and hence globally.
Known convex-position improvements do not transfer directly because they use cap and cyclic-order structure.

Evidence and scope

notes/baseline-review.md
notes/source-audit-manifest.json
records/research-state.json
tools/check_h8.py, SHA-256 8d27a62a4c9c4d2761de683b3af9e99519c1ea13895fb63d1b936a0b762deefd
.proof-experiments/20260721-084327-476459/experiment.json, SHA-256 b40e9924d67225a39b6164741816909c410004105244ee8fdc9c93d1cb6ee63e
.proof-experiments/20260721-084327-476459/stdout.txt, SHA-256 e7cc380cd4a595dea0a4c9a75126b19a2655021120d5c35269c94b937dfafaf8
python3 tools/check_h8.py; return code 0
python3 -m json.tool records/research-state.json and notes/source-audit-manifest.json; both passed
git diff --check; passed

Computational experiments

.proof-experiments/20260721-084327-476459: return code 0; controls passed; eight local counts were 3 and the global count was 4; exact scope was the eight displayed H8 points.

Independent checker

tools/check_h8.py is a dependency-free Python checker written separately from the historical Lean proof and uses exact quadratic-ring pairs. The historical Lean source supplies a materially different formal encoding, but it was not freshly kernel-rebuilt because only 1.4 GB was free and compatible Mathlib build objects were absent.

Contribution gate

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome: progress
Public classification: progress

Cross-domain transfers tested

Few-distance classifications -> the first numerical counterexample junction occurs at the unique 12-point five-distance extremizer -> primary coordinates and collinearity remain to be checked.
Convex isosceles-triangle bounds -> a general-position improvement would improve the local lower bound -> source inspection showed the known improvement relies essentially on convex caps, so direct transfer was rejected.
Historical Lean H8 proof -> predict an exact algebraic replay with local count 3 and global count 4 -> the independent Python calculation reproduced those values.

Established facts

The maintained source lists the global assertion open/falsifiable and explicitly says the local strengthening is false.
https://www.erdosproblems.com/1082, accessed 2026-07-21; retrieved-page hash in notes/source-audit-manifest.json · Maintained status, page last edited 2026-04-11. · proved
The explicit H8 set has no collinear triple, three local nonzero distances at every point, and four global distances.
.proof-experiments/20260721-084327-476459 and tools/check_h8.py · Eight explicit Z[sqrt(3)] coordinates. · computed
Szemerédi's argument gives ceil((n-1)/3) distances from some point.
Erdős 1975 p.101; Sheffer arXiv:1406.1949 Lemma 3.1; Nivasch et al. 2013 section 2. · Every finite planar set with no three collinear. · proved
The current Formal Conjectures statement uses floor division, off-diagonal global distances, and subtraction of the local self-distance.
Formal Conjectures commit b8b5208aa5d01f5f91c49ca516bf09cae8d93693 and source hashes in notes/source-audit-manifest.json · Source-level semantic audit; not a fresh build. · proved

Ruled out in this epoch

Use H8 as a global counterexample.
The explicit Harborth-Fishburn eight-point set. · It has four global distances, exactly floor(8/2). · .proof-experiments/20260721-084327-476459/stdout.txt · None for H8 itself; a different exact configuration is required.
Transfer convex-position local improvements directly to arbitrary no-three-collinear sets.
The Dumitrescu and Nivasch-Pach-Pinchasi-Zerbib cap/good-edge methods. · Their improvement uses strict convexity and cyclic order, neither implied by noncollinearity. · Nivasch et al. 2013, sections 2-4. · A proved replacement for the cap/good-edge lemmas using only NonTrilinear hypotheses.
Use unrestricted g(k) values without inspecting extremal configurations.
Planar few-distance classifications through k=6. · Extremizers may contain collinear triples. · Wei 2012 and the unresolved Shinohara coordinate audit. · Primary exact coordinates, all-triples determinant check, and verified classification coverage.
Freshly rebuild the historical H8 Lean proof during this epoch.
The shared Formal Conjectures checkout. · Only 1.4 GB was free and the required Mathlib build cache was absent. · Filesystem and checkout inspection summarized in notes/baseline-review.md. · At least 6 GB verified free or a complete compatible shared .olean cache.

Open leads

Exact audit of Shinohara's unique 12-point five-distance extremizer.
It is the first classified k-distance extremizer large enough to meet the numerical counterexample threshold. · Encode the primary coordinates in triangular-lattice integer pairs and verify exactly five norms plus every determinant, with positive and negative controls. · high · open
Focused search for later general-position isosceles-triangle bounds.
A strict improvement in the quadratic isosceles count transfers mechanically to a better local distance bound. · Trace citations from Pach-Tardos and Nivasch et al.; translate every applicable bound through the explicit equal-radius-pair inequality before retaining it. · normal · open
Generic exact quadratic-field certificate checker.
It becomes useful only after a sourced candidate family is identified. · Parameterize the ring discriminant and JSON coordinates, then require a separate SymPy or Lean replay for any candidate. · low · open

Continuation checkpoint

Objective: Resolve the first few-distance classification junction without open-ended search.

First action: Obtain Shinohara 2008, DOI 10.1016/j.disc.2007.08.028, or an author-hosted exact coordinate description; verify its uniqueness theorem and encode only the displayed 12-point set.

Stop condition: Stop if primary coordinates or uniqueness cannot be sourced, the set does not have exactly five distances, or the theorem does not cover every 12-point five-distance set; otherwise record only the rigorously implied n <= 13 scope.

Next moves

Obtain Shinohara's primary coordinate description for the unique 12-point five-distance set.
Encode it in triangular-lattice integer coordinates and exactly check the norm u^2+uv+v^2, all squared distances, and all triple determinants.
If it has a collinear triple and the uniqueness theorem has the required scope, derive only the resulting n <= 13 corollary.
Do not begin open-ended candidate generation until this classification junction is resolved.

Citations

Tool disclosure

GPT-5.6 Sol principal performed synthesis, source audit, experiment design, artifact editing, and adversarial checks. A GPT-5.6 Terra source-discriminator delegate supplied an advisory memo and initial checker; the Sol principal independently retrieved sources, inspected the promoted files, modified controls, and reran the calculation. Python 3.12.3 executed exact arithmetic and the experiment recorder. curl, pdftotext, Crossref, OpenAlex, Semantic Scholar, Git, and shell text tools supported retrieval and audit. Lean 4.27.0 and Formal Conjectures source were inspected, but the historical proof was not freshly compiled. No CAS, SAT/SMT solver, or external human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 1352.8s
Review state: not a result claim
Attempt ID: erdos-1082-20260721-085234-e90afe

Human review ledger

No human review recorded.