INDEPENDENT REBUILD AUDIT: Lean formalization of Paper I, Delcourt–Postle, "A Proof of Nash-Williams' Conjecture" (arXiv:2606.11178) ===================================================================================================== Status: an independent rebuild of an outside result that has not been refereed. The mathematics is by Michelle Delcourt and Luke Postle. The Lean formalization is by Juan Pablo Traverso Gianini, written with AI assistance as disclosed in its formalization.yaml. This receipt only records what one machine checked. It is not a review of the paper and it is not an endorsement. Auditor: Ford (P42), on a redacted research machine, Sun Nov 1 2026, 5:56–6:46 PM MST (UTC-7). Everything ran at nice 19, limited to 8 cores (taskset 12-19), inside ~/ford/nashwilliams. The audited clone was not modified: `git status --porcelain` was empty before and after. 0. FALSIFIERS (fixed by the task brief before the build started) F1 `lake build` fails at the pinned commit with the repo's own toolchain and Mathlib pin. F2 `#print axioms` on any main theorem shows something besides propext / Quot.sound / Classical.choice (for example sorryAx, Lean.ofReduceBool from native_decide, or a custom axiom). F3 The formal statement does not match the paper: hypotheses that are missing, extra or vacuous, or definitions that differ from the standard notions. F4 The Challenge (statement) file and the Solution file elaborate to different statements, or their hashes differ from the Palomar registry entry. F5 An independent kernel (not Lean's own) rejects the exported proof terms. Result: none of F1–F5 fired. (Details below.) 1. PINNED SOURCE Repo: https://github.com/jtraverso/nash-williams-lean Commit: 2603197abdbf0a600ec663f6f046f70fbd209d4a (2026-10-20 11:51 AM MDT; "Publish official English preprint 1.0 and formalization companion") Release: https://github.com/jtraverso/nash-williams-triangle-decompositions-release Registry: Palomar PALOMAR-2026-10-21-000009 v1 Toolchain: leanprover/lean4:v4.35.0-rc3 (release candidate; Lake 5.0.0-src+470d5ce, which matches Palomar's toolchain_commit 470d5ce). The project uses the module system. Mathlib: c55e6e786f49471c72fbddbec5415808896aec1e (the repo's own pin; the same pin as our #742 audit) Size: 1,071 .lean files, 201,944 lines (the README says 1,070 project modules). The libraries are RequestProject, PartitionedTriangleAbsorption (Paper II typed absorption, in-tree), Challenge and Solution. sha256: Challenge.lean a0e5c5ba733e05bc8a33edd9ae8abcbd0aebfa2643b6d612f5408b85f2c3ced0 (6,517 bytes) Solution.lean d4d6871581fc79935d0904b2dc16ffe38892906f5c2cd23fa298ff261757f06a Both are byte-identical to Palomar challenge_sha256 / solution_sha256. 2. BUILD (F1: did not fire) `lake exe cache get`: 8,942 Mathlib files decompressed, 0 downloaded, rc 0. `lake build`: rc 0. "Build completed successfully (10031 jobs)." Started 5:57:40 PM MST and ended 6:15:15 PM MST, so the wall time was 1,055 s (17.6 min) on 8 cores at nice 19, with Mathlib coming from cache. The only `declaration uses sorry` warnings are the 3 in Challenge.lean (lines 98, 108, 118). That is the statement-only file, so they are expected. Its theorems are not used by Solution. The other warnings are deprecations (if_pos/if_neg/push_neg/...), unused-variable and unused-simp-arg linters, and "Try this" suggestions. None of them are errors. Log: ~/ford/nashwilliams/build_full.log (summary in build.out) 3. AXIOMS (F2: did not fire) [AuditAxioms.lean, `lake env lean`, 8.7 s] 'NashWilliamsTheorem.nash_williams' depends on axioms: [propext, Classical.choice, Quot.sound] 'NashWilliamsTheorem.fractional_nash_williams' depends on axioms: [propext, Classical.choice, Quot.sound] 'NashWilliamsTheorem.fractional_stability' depends on axioms: [propext, Classical.choice, Quot.sound] 'NashWilliams18.PaperI.nash_williams_via_paperII' depends on axioms: [propext, Classical.choice, Quot.sound] 'NashWilliams18.PaperII.theorem146_F0' depends on axioms: [propext, Classical.choice, Quot.sound] 'NashWilliams18.PaperII.theorem147_F1' depends on axioms: [propext, Classical.choice, Quot.sound] 'NashWilliams18.PaperII.theorem147_F2' depends on axioms: [propext, Classical.choice, Quot.sound] 'NashWilliams.Frac.exists_fractional_weights' depends on axioms: [propext, Classical.choice, Quot.sound] 'NashWilliams.Frac.theorem_1_6_proof' depends on axioms: [propext, Classical.choice, Quot.sound] None of these depend on sorryAx, Lean.ofReduceBool or a custom axiom. The source's own `#print axioms` lines that show up in the build log: 283 x [propext, Classical.choice, Quot.sound], 6 x [propext, Quot.sound], 5 x [propext]. None is outside the standard three. Escape-hatch grep over all 1,071 tracked .lean files: - Zero hits for native_decide, unsafe, implemented_by, opaque, csimp, run_cmd, #eval, ofReduceBool and debug options. - `sorry` appears only in Challenge.lean (x3) and in comments. - `admit` appears only as the English word "admits". - `axiom` appears only in one docstring. - There are 13 local tactic `macro` shorthands, which are benign. - set_option is used only for maxHeartbeats, maxRecDepth, hygiene, linter and exponentiation.threshold. - 8 x `simp (config := {decide := true})`, which is kernel decide, not native. - External inputs are written as named propositions in BKLOInterface.lean and as h1316 hypotheses in Cases.lean. The final theorems carry none of these hypotheses, and the axiom output above shows nothing left assumed. 4. INDEPENDENT KERNELS (F5: did not fire) `leanexport Solution -- ` exported the transitive closure: 726,233,449 bytes, sha256 21f87e328f1dc25da64b4281e9e7ec7e13c716f590ff629b4957150d08157485, in 34.5 s. - nanoda 0.4.17 (an independent Rust kernel), with permitted_axioms = [propext, Classical.choice, Quot.sound], unpermitted_axiom_hard_error = true and the Nat/String extensions on: "Checked 62724 declarations with no errors". It took 69.5 s, rc 0. The only axioms in the export are those three. nanoda's pretty-print of the 3 theorems matches the statements quoted below. - con-ron --verified --jobs=4: "accepted 60511 declarations (--verified)". It took 53.2 s, rc 0. (Its count differs from nanoda's because it models Lean.Syntax in-process; it reports this.) - leanchecker --fresh Solution (Lean's own kernel replaying the whole import closure, Mathlib plus the project): PASSED. Started 6:20:49 PM MST, ended 7:03:26 PM MST (wall 42:37, user 2481 s, max RSS 8.7 GiB), nice 19, cores 12-15, exit status 0, no errors printed. Log ~/ford/nashwilliams/leanchecker.out, sha256 ed1ccb21c9e020ae000b0d48ae5ac8668499bd54adca8c9c25cf6be1ec05d3e1 (942 bytes). Checked 7:29 PM MST. These are the same two external kernels that Palomar lists (nanoda, con-ron), rerun here independently. 5. STATEMENT MATCH (F3, F4: did not fire, with the disclosed caveat on Theorem 1.6) Verbatim (Challenge.lean = Solution.lean). These definitions use Mathlib only (SimpleGraph, IsNClique, cliqueFinset, edgeFinset, degree, minDegree): abbrev IsTriangle (G : SimpleGraph V) (t : Finset V) : Prop := G.IsNClique 3 t def IsTriangleDecomposition (G : SimpleGraph V) (D : Finset (Finset V)) : Prop := (∀ t ∈ D, IsTriangle G t) ∧ ∀ u v, G.Adj u v → ∃! t, t ∈ D ∧ u ∈ t ∧ v ∈ t def HasTriangleDecomposition (G : SimpleGraph V) : Prop := ∃ D, IsTriangleDecomposition G D def IsTriangleDivisible (G : SimpleGraph V) [DecidableRel G.Adj] : Prop := 3 ∣ G.edgeFinset.card ∧ ∀ v, Even (G.degree v) theorem nash_williams : ∃ N : ℕ, ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], N ≤ Fintype.card V → NashWilliams.IsTriangleDivisible G → 3 * Fintype.card V ≤ 4 * G.minDegree → NashWilliams.HasTriangleDecomposition G theorem fractional_nash_williams {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hδ : 3 * Fintype.card V ≤ 4 * G.minDegree) : ∃ w : Finset V → ℝ, (∀ t, 0 ≤ w t) ∧ ∀ u v, G.Adj u v → ∑ t ∈ G.cliqueFinset 3 with u ∈ t ∧ v ∈ t, w t = 1 theorem fractional_stability : ∃ σ₀ : ℝ, 0 < σ₀ ∧ ∀ σ : ℝ, 0 < σ → σ ≤ σ₀ → ∃ ε : ℝ, 0 < ε ∧ ∃ n₀ : ℕ, ∀ (W : Type) [Fintype W] [DecidableEq W] (Gr : SimpleGraph W) [DecidableRel Gr.Adj], n₀ ≤ Fintype.card W → (3 / 4 - ε) * (Fintype.card W : ℝ) ≤ (Gr.minDegree : ℝ) → ¬ NashWilliams.HasFractionalTriangleDecomposition Gr → NashWilliams18.IsExtremal σ Gr (IsExtremal σ G: at least (1-σ)n vertices have degree ≤ (3/4+σ)n, and some S ⊆ V has cutSize ≥ (1-σ)n²/4.) Against the paper (arXiv:2606.11178): - nash_williams vs Conjecture 1.1 / Theorem 1.8 ("Let G be a K3-divisible graph with n vertices and δ(G) ≥ 3n/4. If n is sufficiently large, then G admits a K3-decomposition."): - "sufficiently large" corresponds to ∃ N, N ≤ n. - K3-divisible (3 | e(G), every degree even) corresponds to IsTriangleDivisible. - δ ≥ 3n/4 is exactly 3n ≤ 4δ in ℕ. - A K3-decomposition means every member of D is a triangle of G and every edge lies in exactly one member, which is an edge partition into triangles. MATCH. - fractional_nash_williams vs Theorem 1.4 (δ ≥ 3n/4 gives a fractional K3-decomposition): nonnegative weights on triangles, summing to 1 over the triangles through each edge. There is no large-n condition, which is the same as the paper. MATCH. - fractional_stability vs Theorem 1.6: WEAKER THAN THE PAPER, as disclosed. The Lean statement adds an order threshold n₀ that Theorem 1.6 does not have; formalization.yaml discloses this as a divergence. The rest matches: "some cut ≥ (1-σ)n²/4" is equivalent to "max cut ≥ (1-σ)n²/4", and "sufficiently small σ" corresponds to σ ≤ σ₀. - Challenge vs Solution: `#check`/`#print` with pp.all of the 3 theorems and 8 definitions were byte-identical (20,167 bytes each). - My own non-vacuity file (NonVacuity.lean; rc 0; standard axioms only) checks two things: - For every k ≥ 1, K_{6k+1} is triangle-divisible and satisfies 3n ≤ 4δ. So the hypotheses of nash_williams hold for arbitrarily large n, and the theorem is not vacuous. - The 1-edge graph K2 has no triangle decomposition, so the conclusion is not trivially true. 6. PALOMAR COMPARISON These match what I found: commit 2603197a, toolchain v4.35.0-rc3 / 470d5ce, permitted axioms {propext, Quot.sound, Classical.choice}, theorem_names (the 3 above), challenge/solution sha256, challenge_bytes 6517, and kernels {nanoda, con-ron} (rerun here, both accept). Other fields: - Palomar's review outcome is "neutral" (reviewer codex:gpt-6-sol, no warnings). - Delcourt–Postle author_endorsement is "not-contacted". - Palomar's verified_at is 2026-10-20 2:36 PM MDT. 7. VERDICT PASS. It builds cleanly at the pinned commit. The 3 main theorems depend only on the standard axioms. Two independent kernels (nanoda, con-ron) accept the exported proof closure, and Lean's own leanchecker --fresh replay of the full import closure also passes (rc 0). Challenge and Solution are identical and match the registry hashes. - The main theorem (nash_williams) matches Delcourt–Postle's Theorem 1.8 / Nash-Williams' conjecture for sufficiently large n. - The fractional threshold matches Theorem 1.4. - Fractional stability is a disclosed weakening of Theorem 1.6 (extra n₀). 8. CAVEATS / OPEN ITEMS - The paper is a preprint and has not been refereed. The Lean code is AI-assisted (Aristotle/Harmonic, Claude Opus 5.5, ChatGPT/Codex per formalization.yaml), and its review is "agent-reviewed only; no independent human review." Lean checks the logic of the stated theorems. It does not check the paper's refereeing. - The proof does NOT use Delcourt–Postle's Theorem 13.16. It replaces it with Paper II typed absorption (in-tree as PartitionedTriangleAbsorption, PaperII.theorem146_F0 / theorem147_F1/F2) plus a protected covering round. So the formal route differs from the paper's at that step. All of it is machine-checked here. - It uses a local copy of Ehard–Glock–Joos Thm 1.2 (Pseudorandom.theorem_1_2; also formalized as PALOMAR-2026-10-17-000004). This is proved in-tree, not assumed. - The thresholds N, n₀, ε are existential, not explicit. - Vertex types are in universe 0 (`Type`). This is harmless, because every finite graph is isomorphic to one on Fin n. - The toolchain is a release candidate (v4.35.0-rc3) and the project uses the module system. - I did not run the author's tools/check_palomar.py, because it writes tools/check_report.txt into the repo. I reproduced its checks independently (identity, axioms, grep). - Paper II (jtraverso/typed-triangle-absorption @ 673c6d4) is NOT audited here. Its size is 1,514 .lean files, about 44.1 MB of source (GitHub tree API). The Paper II material that Paper I depends on is built in-tree as part of this audit. 9. REPRODUCE git clone https://github.com/jtraverso/nash-williams-lean && cd nash-williams-lean git checkout 2603197abdbf0a600ec663f6f046f70fbd209d4a nice -n 19 lake exe cache get && nice -n 19 lake build nice -n 19 lake env lean ../AuditAxioms.lean # axioms + #print of definitions nice -n 19 lake env lean ../IdChallenge.lean > a; nice -n 19 lake env lean ../IdSolution.lean > b; cmp a b nice -n 19 lake env lean ../NonVacuity.lean lake env leanexport Solution -- NashWilliamsTheorem.nash_williams NashWilliamsTheorem.fractional_nash_williams \ NashWilliamsTheorem.fractional_stability > solution_export.ndjson nanoda_bin nanoda.json ; con-ron --verified --jobs=4 solution_export.ndjson (Audit files: ~/ford/nashwilliams/{AuditAxioms,IdChallenge,IdSolution,NonVacuity}.lean, nanoda.json and *.out) 10. CREDITS Mathematics: Michelle Delcourt and Luke Postle (arXiv:2606.11178). Formalization: Juan Pablo Traverso Gianini (jtraverso), with AI assistance as disclosed. Independent kernels: nanoda (ammkrn), con-ron. Mathlib community.