Ford receipt: independent kernel check and statement-fidelity review of OpenAI's Lean proof for Erdős #802
(openai/math family 184, theorem OAI.CliqueFreeLog.logarithmic_independence_bound)
Run: 2026-10-26 23:50 to 2026-10-27 00:00 MDT on Kevin's remote ARM64 Linux workstation, Lean v4.34.1, Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612
Source: https://github.com/openai/math at 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a (Apache-2.0)
  challenge lean/ComparatorChallenges/CliqueFreeLog.lean sha256 f2da8879eb520c1fcc7812d3d476f528b54dd7405c00a8f4c0488e212379c2d2
Follows Ford's compile receipt /data/ford_receipts/oai184_lean_check.txt (same build, same pins).

WHAT THIS IS: a re-check of OpenAI's proof. It is not P42's proof, and P42 makes no claim about who proved what first.
Whether Erdős #802 counts as solved is erdosproblems.com's call, not ours.

=== Falsifier (written before anything in this review was run; host name redacted)
Ford review 2026-10-26 23:50 MDT. Target: openai/math @ 7ef5c0c family 184, theorem OAI.CliqueFreeLog.logarithmic_independence_bound
(already compiled on the remote workstation [host name redacted], receipt oai184_lean_check.txt). Written BEFORE running anything in this review.
The claim "OpenAI's Lean proof of the CliqueFreeLog statement is kernel-sound AND the statement is a faithful formalisation of Erdős #802" is FALSIFIED if any of:
 K1 an independent checker (lean4export + nanoda_lib / lean4lean, or at minimum lean4checker replaying the oleans in a fresh kernel) rejects any declaration in the theorem's dependency closure;
 K2 the axioms reported by the independent run include anything outside {propext, Classical.choice, Quot.sound};
 S1 the quantifier order lets c depend on anything other than r (e.g. on V, G, n, d);
 S2 averageDegree is not 2|E|/n (e.g. max degree, min degree, or a definition that is degenerate);
 S3 a hypothesis is vacuous: no K_r-free graph with averageDegree >= 2 exists for some r >= 4 (Ford will exhibit one in Lean), or CliqueFree / indepNum mean something other than "no r-clique" / "maximum independent set size";
 S4 the statement differs from #802 as written on erdosproblems.com in a way that changes its content (beyond: d >= 2 normalisation, natural log, finite vertex types in universe 0, r >= 4 since r = 3 is AKS 1980/Shearer);
 S5 erdosproblems.com, its forum, or teorth/erdosproblems already records #802 as solved by someone else (novelty misstatement), or OpenAI's own text claims something different from the Lean theorem.
Controls: a planted sorry in the exported closure must be rejected/flagged by the independent checker (or a tampered olean must be rejected by lean4checker).

=== Part 1. Independent kernel check
Exporter: lean4export (github.com/leanprover/lean4export, tag v4.34.0 = 076e8e57707e813375e8f9da8bf989799ace9680), built with Lean v4.34.1.
  Exported the dependency closure of FordCheckCheck.challenge (Ford's own retyped copy of the challenge statement and averageDegree,
  closed by `exact OAI.CliqueFreeLog.logarithmic_independence_bound r hr`) and of the OpenAI theorem itself.
  Export: 6,168,654 lines of NDJSON (format 3.1.0), sha256 029ec30918861dec7bc52101e20248bcb6aa36fc29bfecd2fa68291e9e5aac0e
  Axiom declarations anywhere in the export: propext, Quot.sound, Classical.choice, and nothing else.
Checker: nanoda_lib (github.com/ammkrn/nanoda_lib @ 37cb87b7e6cd6862ef2bd121faa9f4604f59fe96), an external Lean 4 type checker
  written in Rust, independent of Lean's C++ kernel. rustc 1.99.1. Config: permitted_axioms = [propext, Classical.choice, Quot.sound],
  unpermitted_axiom_hard_error = true, Nat and String kernel extensions on (standard accelerated literals).
--- nanoda output (the statements below are printed by nanoda from the export, not by Lean)
theorem FordCheckCheck.challenge (r : Nat) (hr : LE.le (OfNat.ofNat 4) r) :
  Exists
    (fun (c : Real) =>
    And (LT.lt (OfNat.ofNat 0) c)
      (forall {V : Type 0} [inst._@.FordCheck.Check.762970257._hygCtx._hyg.31 : Fintype V]
        (G : SimpleGraph V),
      SimpleGraph.CliqueFree G r → LE.le (OfNat.ofNat 2) (FordCheckCheck.averageDegree G) → LE.le
        (HDiv.hDiv
          (HMul.hMul (HMul.hMul c (Nat.cast (Fintype.card V))) (Real.log (FordCheckCheck.averageDegree G)))
          (FordCheckCheck.averageDegree G)) (Nat.cast (SimpleGraph.indepNum G)))) :=
  _

theorem OAI.CliqueFreeLog.logarithmic_independence_bound (r : Nat) (hr : LE.le (OfNat.ofNat 4) r) :
  Exists
    (fun (c : Real) =>
    And (LT.lt (OfNat.ofNat 0) c)
      (forall {V : Type 0} [inst._@.OAI.Combinatorics.CliqueFree.Main.4092724696._hygCtx._hyg.31 : Fintype V]
        (G : SimpleGraph V),
      SimpleGraph.CliqueFree G r → LE.le (OfNat.ofNat 2) (OAI.CliqueFreeLog.averageDegree G) → LE.le
        (HDiv.hDiv
          (HMul.hMul (HMul.hMul c (Nat.cast (Fintype.card V))) (Real.log (OAI.CliqueFreeLog.averageDegree G)))
          (OAI.CliqueFreeLog.averageDegree G)) (Nat.cast (SimpleGraph.indepNum G)))) :=
  _

def FordCheckCheck.averageDegree.{u_1} :
  forall {V : Type u_1} [inst._@.FordCheck.Check.1032556259._hygCtx._hyg.3 : Fintype V],
  SimpleGraph V → Real :=
  fun {V : Type u_1} [inst._@.FordCheck.Check.1032556259._hygCtx._hyg.3 : Fintype V] (G : SimpleGraph V) =>
  HDiv.hDiv (HMul.hMul (OfNat.ofNat 2) (Nat.cast (Finset.card (SimpleGraph.edgeFinset G))))
    (Nat.cast (Fintype.card V))

axiom propext {a b : Prop} : Iff a b → Eq a b

axiom Quot.sound.{u} {α : Sort u} {r : α → α → Prop} {a b : α} :
  r a b → Eq (Quot.mk r a) (Quot.mk r b)

axiom Classical.choice.{u} {α : Sort u} : Nonempty α → α

Checked 46880 declarations with no errors
	Elapsed (wall clock) time (h:mm:ss or m:ss): 0:21.67
	Maximum resident set size (kbytes): 365860
--- Controls
  C-sorry   export of a theorem `bad : False := sorry` -> nanoda: "export file declares unpermitted axiom sorryAx" (exit 1). As required.
  C-tamper  the challenge export with the proof term of FordCheckCheck.challenge swapped for the proof of Nat.zero_le
            -> nanoda panics "assertion failed: self.def_eq(u, v)" (exit 101, rejected). As required.
Second checker: leanchecker (Lean's bundled replay checker, formerly lean4checker; Lean's own kernel, fresh replay of the .olean files)
  on all 31 OAI.Combinatorics.CliqueFree modules plus FordCheck.Check: 32 of 32 OK.
K1: not fired. K2: not fired.

=== Part 2. Statement fidelity
#802 on erdosproblems.com (read 2026-10-27): "Is it true that any K_r-free graph on n vertices with average degree t contains an
independent set on >>_r (log t / t) n many vertices?" Conjecture of Ajtai, Erdős, Komlós, Szemerédi [AEKS81]; r = 3 proved in [AKS80].
Lean statement, as nanoda prints it above:
  for all r : Nat, 4 <= r -> exists c : Real, 0 < c and for all (V : Type) [Fintype V] (G : SimpleGraph V),
     G.CliqueFree r -> 2 <= averageDegree G -> c * |V| * Real.log (averageDegree G) / averageDegree G <= G.indepNum
  with averageDegree G = 2 * |E(G)| / |V| (real division).
 S1 quantifier order: `exists c` comes after r and before V and G, so c depends only on r (the >>_r of the problem). Not fired.
 S2 average degree is 2|E|/n, not max or min degree (definition printed above; Ford's own copy matches the OpenAI one definitionally,
    checked by nanoda through the closure). For n = 0 Lean gives 0, which the hypothesis 2 <= d excludes. Not fired.
 S3 vacuity: Ford proved in Lean that for every r >= 4 and every D there is a K_r-free graph with average degree >= 2 and >= D
    (K_(m,m) with m = D+2, via its 2-colouring and its m*m edges), so the hypotheses are satisfiable at every degree. CliqueFree r is
    Mathlib's "no r-clique"; indepNum is Mathlib's maximum independent-set size. Not fired.
 S4 differences from the problem text, and why none changes its content:
    - r >= 4 only: Ford proved in Lean that the theorem gives the same bound for EVERY r (r <= 3 via Mathlib's CliqueFree.mono), stated
      in the shape of the google-deepmind/formal-conjectures erdos_802 statement on Fin n graphs (FordFid.fc_style below).
    - d >= 2: for d <= 1 the bound is <= 0 and trivial; for 1 < d < 2 the elementary bound alpha >= n/(d+1) > n/3 already gives it
      (log d / d < 1/2), so the restriction only changes the constant. This step is a paper argument, not formalised by Ford.
    - natural log changes only the constant. Finite vertex types in Type 0: the problem is about finite graphs. Not fired.
    OpenAI's paper (Theorem 1.1) states exactly the Lean statement: r >= 4, average degree d >= 2, natural log, c_r uniform in n and d.
--- FordCheck/Fidelity.lean (sha256 5bef174e9f8ecd982d59918d2c9bd16e750971ba2323ed7871608663df189f21), compiled in 9.6 s:
import OAI.Combinatorics.CliqueFree.Main

/-! Ford fidelity checks for OAI.CliqueFreeLog.logarithmic_independence_bound vs Erdős #802. -/

namespace FordFid
open OAI.CliqueFreeLog

/-- (A) Transfer: the OpenAI theorem gives the formal-conjectures-style shape of #802 for EVERY r
(r ≤ 3 by clique-freeness monotonicity), on `Fin n` graphs, with `c` chosen before `n` and `G`,
restricted to average degree ≥ 2. -/
theorem fc_style (r : ℕ) : ∃ c > (0 : ℝ), ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
    G.CliqueFree r → 2 ≤ averageDegree G →
      c * (Real.log (averageDegree G) / averageDegree G) * n ≤ G.indepNum := by
  obtain ⟨c, hc, h⟩ := logarithmic_independence_bound (max r 4) (le_max_right _ _)
  refine ⟨c, hc, fun n G hG hd => ?_⟩
  have := h G (hG.mono (le_max_left _ _)) hd
  simp only [Fintype.card_fin] at this
  calc c * (Real.log (averageDegree G) / averageDegree G) * n
      = c * (n : ℝ) * Real.log (averageDegree G) / averageDegree G := by ring
    _ ≤ _ := this

/-- K_{m,m} is K_r-free for every r ≥ 3. -/
theorem kmm_cliqueFree (m r : ℕ) (hr : 3 ≤ r) :
    (completeBipartiteGraph (Fin m) (Fin m)).CliqueFree r :=
  (SimpleGraph.CompleteBipartiteGraph.bicoloring (Fin m) (Fin m)).colorable.cliqueFree
    (by simp; omega)

/-- K_{m,m} has m² edges (any Fintype instance on the edge set). -/
theorem kmm_edges (m : ℕ) [Fintype (completeBipartiteGraph (Fin m) (Fin m)).edgeSet] :
    ((completeBipartiteGraph (Fin m) (Fin m)).edgeFinset.card : ℕ∞) = m * m := by
  have h := SimpleGraph.encard_edgeSet_completeBipartiteGraph (W₁ := Fin m) (W₂ := Fin m)
  rw [← SimpleGraph.coe_edgeFinset, Set.encard_coe_eq_coe_finsetCard] at h
  simpa using h

/-- K_{m,m} has average degree m (m ≥ 1). -/
theorem kmm_avg (m : ℕ) (hm : 1 ≤ m) :
    averageDegree (completeBipartiteGraph (Fin m) (Fin m)) = m := by
  classical
  unfold averageDegree
  have he := kmm_edges m
  have he' : ((completeBipartiteGraph (Fin m) (Fin m)).edgeFinset.card : ℕ) = m * m := by
    exact_mod_cast he
  simp only [Fintype.card_sum, Fintype.card_fin]
  rw [show ((completeBipartiteGraph (Fin m) (Fin m)).edgeFinset.card : ℝ) = (m * m : ℕ) by
    convert congrArg (fun k : ℕ => (k : ℝ)) he']
  have : (m : ℝ) ≠ 0 := by exact_mod_cast (by omega : m ≠ 0)
  push_cast
  field_simp
  ring

/-- (B) Non-vacuity: for every r ≥ 4 the hypothesis class of the OpenAI theorem contains graphs of
arbitrarily large average degree, so it is not satisfied vacuously. -/
theorem nonvacuous (r : ℕ) (hr : 4 ≤ r) (D : ℕ) :
    ∃ (V : Type) (_ : Fintype V) (G : SimpleGraph V),
      G.CliqueFree r ∧ 2 ≤ averageDegree G ∧ (D : ℝ) ≤ averageDegree G := by
  refine ⟨Fin (D + 2) ⊕ Fin (D + 2), inferInstance, completeBipartiteGraph _ _,
    kmm_cliqueFree _ _ (by omega), ?_, ?_⟩ <;>
  · rw [kmm_avg _ (by omega)]; push_cast; linarith [(Nat.cast_nonneg D : (0:ℝ) ≤ D)]

end FordFid

#print axioms FordFid.fc_style
#print axioms FordFid.nonvacuous

--- output
'FordFid.fc_style' depends on axioms: [propext, Classical.choice, Quot.sound]
'FordFid.nonvacuous' depends on axioms: [propext, Classical.choice, Quot.sound]
exit 0

=== Part 3. Public record (read 2026-10-27)
- OpenAI released the repository on 2026-10-06 ("Sharing AI progress in mathematics", openai.com). Its paper (dated 2026-09-25) says the
  theorem gives a positive answer to the conjecture of Ajtai, Erdős, Komlós and Szemerédi, "also recorded as Erdős Problem 802".
  The repository says its manuscripts were produced by an unnamed internal OpenAI model. The paper is not refereed.
- T. F. Bloom's erdosproblems.com blog post of 2026-10-08 ("Erdős problems in the OpenAI proofs") lists #802 as a formalised claim and
  says the list is not an endorsement and that he had not yet checked the Lean files.
- The erdosproblems.com page for #802 shows no proof claim and no solved label.
  The teorth/erdosproblems database still records it as open (last updated 2025-08-31).
- erdosproblems.ai, a separate wiki, already lists #802 as proved, citing its own build of the same Lean declaration and its own
  statement-fidelity audit. So P42 is not the first to re-check this proof. This receipt adds a check by an external kernel (nanoda).
S5: not fired. No source credits #802 to anyone else, and OpenAI's text matches the Lean theorem.
Correction: Ford's earlier receipt and log entry said erdosproblems.com "still lists #802 as open". More precisely, the page carries no
status label at all, no proof claim is filed there, and the site's maintainer treats the OpenAI result as a claim.

=== Verdict
HELD. The proof passes an independent type checker that permits only the three standard axioms. The statement says what #802 asks:
directly for r >= 4, for every r via a one-line step, and up to the harmless d >= 2 normalisation. Not checked: the 21-page paper's
prose argument, any refereed review, and questions of credit. Not our proof. Whether #802 is solved is erdosproblems.com's call.