How much to trust this

The statement to audit

This is the whole of Challenge.lean. It imports only Mathlib’s Finset and uses the textbook definition of a covering design. The two sorrys are the holes that Solution.lean fills.

module

public import Mathlib.Data.Finset.Card

public section

/-!
# Lower bounds for the covering numbers C(24,14,4) and C(25,15,5)

A `(v, k, t)` covering design is a family of `k`-element subsets (blocks) of a `v`-element set
such that every `t`-element subset is contained in at least one block. The covering number
`C(v, k, t)` is the least number of blocks in such a design.

The two theorems below say that `C(24, 14, 4) ≥ 20` and `C(25, 15, 5) ≥ 34`. The point set is
`Fin v`, a family of blocks is a `Finset` of `Finset`s, and no other definitions are used.
-/

/-- Every family of 14-element subsets of a 24-element set that covers every 4-element subset
has at least 20 members. That is, `C(24, 14, 4) ≥ 20`. -/
theorem Covering.Palomar.covering_24_14_4_lower_bound (𝒯 : Finset (Finset (Fin 24)))
    (hk : ∀ B ∈ 𝒯, B.card = 14)
    (hcov : ∀ S : Finset (Fin 24), S.card = 4 → ∃ B ∈ 𝒯, S ⊆ B) :
    20 ≤ 𝒯.card := by
  sorry

/-- Every family of 15-element subsets of a 25-element set that covers every 5-element subset
has at least 34 members. That is, `C(25, 15, 5) ≥ 34`. -/
theorem Covering.Palomar.covering_25_15_5_lower_bound (𝒯 : Finset (Finset (Fin 25)))
    (hk : ∀ B ∈ 𝒯, B.card = 15)
    (hcov : ∀ S : Finset (Fin 25), S.card = 5 → ∃ B ∈ 𝒯, S ⊆ B) :
    34 ≤ 𝒯.card := by
  sorry

Both proved theorems report:

depends on axioms: [propext, Classical.choice, Quot.sound]

The checks

• Checked by Lean

  The proof compiles, with no gaps

  All 80 proof modules build with Lean 4.35.0-rc3 and Mathlib v4.35.0-rc3, with no sorry. Every final theorem depends only on Lean’s three standard axioms.

• Checked by Comparator

  It proves exactly the stated theorem

  Comparator confirms that Solution.lean proves the statements in Challenge.lean, replaying the proof through Lean’s kernel and two independent kernels, NanoDa and con-ron. CI runs it on every push.

• Registered on Palomar

  An independent registry checked it

  Palomar, a registry of Lean-verified results, ran the same check on its own machines and archived the repository at commit 17bca00 as entry PALOMAR-2026-10-04-000003.

• Checked by Lean

  The agents’ definitions mean the textbook ones

  The agents worked with lists of blocks, allowing repeats. IndependentCheck.lean, written afterwards, derives the textbook Finset statement from their theorems. A definition that secretly meant something stronger would make that derivation fail.

• Rebuilt twice

  Fresh rebuilds on two Lean versions

  Every module was rebuilt from source and re-checked with leanchecker on Lean 4.34.1 and 4.35.0-rc3. The records are in the verification folder.

• Not yet reviewed

  A mathematician reading the proof

  Nobody has reviewed the mathematics yet; a review has been requested. Agents reviewed each other during the campaign, which is not peer review.

• Not checked

  This site and PROOF.md match the Lean

  The written explanations were produced by AI from the agents’ notes and the Lean source. Lean checks the formal proof, not this prose. Links to declarations are checked automatically when the site is built.