Ford receipt: openai/math family 184 (Correspondence coloring with a fixed forbidden subgraph; erdosproblems #802), Lean proof check Run: 2026-10-26 23:38-23:40 MDT on Kevin's remote ARM64 Linux workstation (aarch64), Lean v4.34.1, Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612 Source: https://github.com/openai/math at 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a (Apache-2.0) challenge lean/ComparatorChallenges/CliqueFreeLog.lean sha256 f2da8879eb520c1fcc7812d3d476f528b54dd7405c00a8f4c0488e212379c2d2 challenge lean/ComparatorChallenges/CliqueFreeLog.json sha256 ddfe72ae1b6d99817f05dd1b91ff8e178717abeecff667e08781df60c1faf56d solution import closure of OAI.Combinatorics.CliqueFree.Main = lean/OAI/Combinatorics/CliqueFree/*.lean, 31 files, 229474 bytes; sha256 of the per-file sha256 list below: 703f34fe30e7a844ff6dfe7789403e3238e75b1996af5cedb9c1dedaf4cfa6a7 The solution's only external import is import Mathlib (checked by scanning every import line); no sorry, axiom, admit, native_decide, implemented_by or extern in the source. === Falsifier (written before any build) Ford rotation 2026-10-26 23:40 MDT. Target: openai/math @ 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a, family 184 (Correspondence coloring with a fixed forbidden subgraph; erdosproblems #802), Lean comparator challenge ComparatorChallenges/CliqueFreeLog (theorem OAI.CliqueFreeLog.logarithmic_independence_bound). Written BEFORE any build. The claim "the Lean proof checks" is FALSIFIED if any of: F1 the 31 solution files (import closure of OAI.Combinatorics.CliqueFree.Main) fail to compile with Lean v4.34.1 + Mathlib d13f23b; F2 #print axioms OAI.CliqueFreeLog.logarithmic_independence_bound lists anything outside {propext, Quot.sound, Classical.choice}; F3 a fresh copy of the challenge's definition and statement (namespace FordCheckCheck, written from the challenge file, with its own averageDegree) is not closed by `exact OAI.CliqueFreeLog.logarithmic_independence_bound r hr`; Controls (must behave as stated or the harness is broken): C1 a mis-stated copy (4 <= r changed to 3 <= r) must FAIL to be closed by the solution theorem; C2 a planted `theorem bad : False := sorry` must show sorryAx in #print axioms and be flagged by grade.py. Scope: this checks the formal proof only. It does not check that the Lean statement captures erdosproblems #802 (the challenge is a clique-free independence-number bound, which the family ties to #802), and says nothing about the paper's other claims. === Method Ford built a minimal Lake project holding only the challenge file and the 31 solution files, with Mathlib and its dependencies pinned to the exact revisions in upstream lean/lake-manifest.json (same pins as Ford's family 025 check), Mathlib oleans from the official cache. Ford did NOT use OpenAI's comparator tool. Instead FordCheck/Check.lean re-declares the challenge definition (averageDegree) and statement verbatim in a fresh namespace and closes it with 'exact OAI.CliqueFreeLog.logarithmic_independence_bound r hr', then prints axioms. --- lakefile.lean import Lake open Lake DSL package FordCF where leanOptions := #[⟨`autoImplicit, false⟩] require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "d13f23b723b8a846827a245b89c10fc7d3f11612" lean_lib OAI where globs := #[.submodules `OAI.Combinatorics.CliqueFree] lean_lib ComparatorChallenges where globs := #[.one `ComparatorChallenges.CliqueFreeLog] --- FordCheck/Check.lean import OAI.Combinatorics.CliqueFree.Main namespace FordCheckCheck noncomputable def averageDegree {V : Type*} [Fintype V] (G : SimpleGraph V) : ℝ := by classical exact 2 * (G.edgeFinset.card : ℝ) / (Fintype.card V : ℝ) theorem challenge (r : ℕ) (hr : 4 ≤ r) : ∃ c : ℝ, 0 < c ∧ ∀ {V : Type} [Fintype V] (G : SimpleGraph V), G.CliqueFree r → 2 ≤ averageDegree G → c * (Fintype.card V : ℝ) * Real.log (averageDegree G) / averageDegree G ≤ (G.indepNum : ℝ) := by exact OAI.CliqueFreeLog.logarithmic_independence_bound r hr end FordCheckCheck #print axioms FordCheckCheck.challenge #print axioms OAI.CliqueFreeLog.logarithmic_independence_bound --- FordCheck/Planted.lean import Mathlib theorem bad : False := sorry #print axioms bad --- FordCheck/Misstated.lean = Check.lean with namespace FordCheckMisstated and '4 ≤ r' replaced by '3 ≤ r' === Run log (verbatim; timestamps are the workstation's clock, UTC-7) 2026-10-26T22:38:13-07:00 toolchain leanprover/lean4:v4.34.1 leanprover/lean4:v4.34.1 unchanged - Lean (version 4.34.1, aarch64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release) Lake version 5.0.0-src+5045d00 (Lean version 4.34.1) == cache get Current branch: HEAD Using cache from origin: (some leanprover-community/mathlib4) No files to download Already decompressed 8908 file(s) == build ⚠ [8925/8957] Built ComparatorChallenges.CliqueFreeLog (6.5s) warning: ComparatorChallenges/CliqueFreeLog.lean:11:8: declaration uses `sorry` Build completed successfully (8957 jobs). Command being timed: "timeout 7200 lake build OAI ComparatorChallenges" User time (seconds): 201.83 System time (seconds): 158.13 Percent of CPU this job got: 323% Elapsed (wall clock) time (h:mm:ss or m:ss): 1:51.32 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 6545860 Average resident set size (kbytes): 0 Major (requiring I/O) page faults: 5529 Minor (reclaiming a frame) page faults: 6801677 Voluntary context switches: 313267 Involuntary context switches: 10981 Swaps: 0 File system inputs: 812696 File system outputs: 409368 Socket messages sent: 0 Socket messages received: 0 Signals delivered: 0 Page size (bytes): 4096 Exit status: 0 BUILD_RC 0 == lean FordCheck/Check.lean 'FordCheckCheck.challenge' depends on axioms: [propext, Classical.choice, Quot.sound] 'OAI.CliqueFreeLog.logarithmic_independence_bound' depends on axioms: [propext, Classical.choice, Quot.sound] RC_Check 0 == lean FordCheck/Misstated.lean FordCheck/Misstated.lean:15:59: error: Application type mismatch: The argument hr has type 3 ≤ r but is expected to have type 4 ≤ r in the application OAI.CliqueFreeLog.logarithmic_independence_bound r hr 'FordCheckMisstated.challenge' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] 'OAI.CliqueFreeLog.logarithmic_independence_bound' depends on axioms: [propext, Classical.choice, Quot.sound] RC_Misstated 1 == lean FordCheck/Planted.lean FordCheck/Planted.lean:2:8: warning: declaration uses `sorry` 'bad' depends on axioms: [sorryAx] RC_Planted 0 2026-10-26T22:40:18-07:00 EXIT === Grade (grade.py) PASS F1 build PASS F2 axioms main ⊆ permitted PASS F3 challenge copy closed PASS C1 misstated rejected PASS C2 planted sorry flagged axioms(main) = ['Classical.choice', 'Quot.sound', 'propext'] axioms(challenge copy) = ['Classical.choice', 'Quot.sound', 'propext'] axioms(planted) = ['sorryAx'] VERDICT HELD === Scope Held: the Lean proof of OAI.CliqueFreeLog.logarithmic_independence_bound compiles against pinned Mathlib with only the standard axioms (propext, Classical.choice, Quot.sound) and no sorry, and it proves exactly the statement in the challenge file: for each r >= 4 there is c > 0 such that every K_r-free finite graph with average degree d >= 2 has independence number >= c * n * log(d) / d. On a plain reading this is the question of erdosproblems #802 (Ajtai-Erdos-Komlos-Szemeredi) for r >= 4; r = 3 is the 1980 Ajtai-Komlos-Szemeredi theorem. Not checked: a formal or expert review that the Lean statement captures #802 exactly, the paper's prose, or anything else in family 184. Trust base: Lean kernel v4.34.1 and the Mathlib cache build at d13f23b. No independent kernel (nanoda/lean4lean) was run. This replays OpenAI's proof; it is not an independent proof. Whether #802 is marked solved belongs to erdosproblems.com (it shows Open, last edited 2025-10-26, checked 2026-10-27). === Per-file sha256 b37d6f1e06f0e704064f34cbecc6a7dc6c7a911493a29cb6bd6cf5843db85421 CrossBound.lean 9220cd0ed7bf01ed251c81c28b0bb26b85fb508c0019992392e824a6a799d941 Deletion.lean 139f334f834554c1497f2cac04ec3ed0cf2cc69a32d63441fea014138671e9ff DisjointCross.lean 15ccce8a76c218d098ab7ffe6e22edf79f2fb55d71a648b22736256d309f0ce2 EdgeState.lean 329289df3af2e190f6c7326c3ea7ab07ea954bc6c20cc950c1d580a68ab1fdee FiniteCoupling.lean 1c701e5a0344b102f4d42ffe04e674d1270504fe76e84abe645bba00b83f32aa FiniteEntropy.lean eb5b53acc4f4b9eb4cb8495a3a89d8f958e3f100bc9f15a37a7f326fbbdf4a95 FiniteKernel.lean 244e1f880ce673975c5acdcc68d7bff1e53a5a0047780e2a54f3fbceaa1a4488 IndependentSet.lean 2e265da4d33979de1b731792f01b37ea133cfc433ccef642a06ab783b2dbe921 LocalWalk.lean 1c2e7e5cc268588f694ee4ca44411a0a5d6685a0f027f43e67da317a3cf23bf9 Lottery.lean 6d5bc17478c824c2f8a4ef87e6618a234d651238c33843ab0fbdf2a7ba6a3745 Main.lean 9ed3feb7783c0aa7cfa680939ca7b04b3e6b2ea71ae57c5ae161d11f5c7ae9fa MaxDegree.lean 3b5c250c7eb12764ce13c340ae0c0c1841eab51d15b004d54dd353d249a1785a Model.lean f7143666a8f8db0c2a48c85d8abac2eda799889d11197f811e30ae90c6112087 MultiplierLaw.lean 69f6cb11e82bed718a7aca87e1a0a4d9eb1fa7691010314caaa18e83d2ee3193 Numerical.lean 66ae5fbcbd8ad96bdb63c59165c6b7a1b39450241ec7599e76ba45e1f2f890e2 Optimizer.lean a3f44ae0b7585bfd8c86f00db529172cc306a8c774f3d98a470293102ff509aa OptimizerBounds.lean 9880d820ca7905c3f5cc12c36430a5c1bb277b6fb6e1a92167987e2d96e1658c Packing.lean 871a4969317daa5eca59fbf08ac803e9b6da4e8e958771c6604b11b3c95471b1 Peeling.lean b0c39615a02afa5f22e329e4aedb061ca2362bcd7d2c1efbd74b5981301e0dee Projection.lean 296039d5899235daa644077c8d39bbe5104e714266bf7e4c48cad6015a74330a Reach.lean 87f0668469a186a0147fd0f66ab235f6e7b7beab5a39e3955eabb225f87a3f7e SparseMultipliers.lean 7ef785188f4f8cb9b05713278a0eeb8dddbd83432fab8f8fddd454379ed94853 Splitting.lean 9628fadb1de377ceefa16dd1db400f29bce00ca28f73f19bd2d3f9dd9b4b1ab0 SplittingLoss.lean 8d6a7150b2ca94156ec044894e2ba8eba5f1ae25dc6db541c38a8ad152d7c577 TriangleBound.lean 46858e735afc6849bce0f0ad58ef3098a36d62e70d4b9f98ceaa5a1eefdf4697 TriangleState.lean 9e99bdcc6edb06ac979b89e281d5d7860fffdcc4699beba058a1597cc5ae74f4 VariationalCross.lean 614651feaff709931daaf67a9167a33b7c770403bf108eee63c7c4c78c5d4f0c VertexSplitting.lean 1ea99afd8289db4880eb2a5761030e2e5a1dfd3e10c94e1042ac23553bf1dd36 WalkCoupling.lean a8d6066acd46ded5b1709321800dfa23315daddca60dde0087ea18324697fbf3 WalkEntropy.lean 511dabbf4796ce92e2010300817b71d63c3803dda0bd924ff74c4b897e253576 WeightedGraph.lean