[Lean] Audit: 11 theorem tasks are false, vacuous, or mis-specified, and 2 Decidable tasks do not reliably test executability

[ImYangC7]

Summary

I audited the 26 distinct Lean tasks in ScienceBoard, their Raw and VM JSON versions, and the Lean 4.14.0 / Mathlib 4.14.0 environment fixed by the repository.

At ScienceBoard commit c8d5010bdba32afc5dfb16472873bed148c39a45, 13 tasks should be quarantined pending correction:

A-02, A-04,
B-01, B-02, B-05, B-06, B-07,
C-05,
D-02, D-03, D-07,
E-01, E-02

The evidence supports three different classifications:

• Nine theorem statements are false as elaborated by Lean: A-02, A-04, B-05, B-06, B-07, C-05, D-02, D-03, and D-07.
• B-01 is provable but formalizes the wrong coprimality predicate. B-02 is provable only because its premises contradict the n ≥ 4 branch.
• E-01 and E-02 do not reliably test executable decision procedures under either current evaluator. Raw accepts a noncomputable classical proof term at the extracted proof state, while VM can place the unchanged declaration under noncomputable section.

The statements occur in both tasks/Raw/Lean and tasks/VM/Lean. The 13 logical tasks therefore correspond to 26 Raw/VM JSON configurations. I have not assumed that both configurations are necessarily included in every published aggregate score.

Reproduction environment

ScienceBoard  c8d5010bdba32afc5dfb16472873bed148c39a45
Lean          4.14.0, commit 410fab728470
Mathlib       4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84
REPL tag      v4.14.0, commit d7545ee63b5334ca70ac88c8768171526cf232fa

The companion file ScienceBoard_Lean_issue_reproductions.lean contains checked evidence for the following claims:

• both A-02 boundary counterexamples;
• the elaborated A-04 type and the α = ω, hidden-cardinal 0 counterexample facts;
• complete proofs showing how B-01 and B-02 pass for the wrong reasons;
• a complete B-05 counterexample using an adversarial Pow instance;
• a complete B-06 countermodel using a transported GF(4) division-ring structure;
• a checked proof that no algebra structure can exist from a four-element field to an eight-element field, the obstruction used in B-07;
• complete C-05 and D-03 counterexamples;
• a checked proof that D-07's alleged finite-moment hypothesis is tautological.

The D-02 disconnected-domain counterexample, the construction of all nested-set instances for B-07, and the Pareto model for D-07 are mathematical countermodels described below. The companion file does not claim to contain full Lean formalizations of those three constructions.

Run the checked file with:

lake env lean ScienceBoard_Lean_issue_reproductions.lean

Classification

Task	Classification	Defect
A-02	False	The strict inequality becomes equality when x = 0 or y = 0
A-04	False	Bare ℵ becomes an arbitrary auto-implicit cardinal
B-01	Mis-specified but provable	Generic IsCoprime is used instead of Nat.Coprime
B-02	Vacuously provable	The Hamilton-path premise includes equal endpoints and contradicts n ≥ 4
B-05	False	An arbitrary Pow instance changes the meaning of IsCyclic
B-06	False	An arbitrary quotient DivisionRing need not agree with quotient multiplication
B-07	False	Set inclusions do not constrain the independent field and algebra structures
C-05	False	The hypotheses do not imply compactness of Y
D-02	False	Bounded derivative on a disconnected set does not imply uniform continuity
D-03	False	The degenerate interval a = b is not excluded
D-07	False	The purported finite p-th moment premise is true by reflexivity
E-01	Unsupported executable task	The task is tied to the open four-cubes problem, while the evaluators accept classical noncomputable completion
E-02	Noncomputable generalization	The target specializes to deciding Nonempty α for an arbitrary opaque type, while the evaluators accept classical noncomputable completion

E-01 is not claimed to be a false proposition or a proven-undecidable predicate. Its classification is limited to benchmark suitability.

Detailed findings

A-02 is false at both boundary variables

The task states:

theorem PT_2 : ack x (y + 1) < ack (x + 1) y := by sorry

Setting x = 0 makes both sides y + 2. Setting y = 0 also makes both sides equal, since ack (x + 1) 0 = ack x 1.

example (y : ℕ) : ¬ ack 0 (y + 1) < ack (0 + 1) y := by
  simp [ack]

example (x : ℕ) : ¬ ack x (0 + 1) < ack (x + 1) 0 := by
  simp [ack]

Adding only 0 < x does not repair the strict inequality. Any strict version must at least exclude both boundary cases, such as by requiring 0 < x and 0 < y, and the resulting statement must then be checked independently. Replacing < with ≤ is another candidate repair that also requires independent verification.

A-04 elaborates to a universally false type

The conclusion is written as:

α.cof = ℵ

With autoImplicit enabled, the bare identifier ℵ is silently introduced as an arbitrary implicit cardinal. The elaborated declaration is:

@ST_2 : ∀ {ℵ : Cardinal} (α : Ordinal),
  α.IsLimit → α < ω_ 1 → α.cof = ℵ

Choose α = ω and the hidden cardinal ℵ = 0. Mathlib proves that ω is a limit ordinal below ω₁ and that its cofinality is nonzero. The likely intended right-hand side is ℵ₀.

B-01 proves a different statement from the intended number theory

The premise is:

h₃ : IsCoprime a p

This resolves to the generic commutative-semiring Bézout predicate, not Nat.Coprime. Over natural numbers its coefficients are nonnegative. Together with Nat.Prime p, the condition forces a = 1.

The companion file contains a complete proof of the official theorem that first derives a = 1 and then finishes by ring arithmetic. The task therefore passes without testing the expected Fermat-style congruence argument. The intended predicate should be Nat.Coprime a p.

B-02 is closed by contradiction, without an edge-count argument

The premise demands a Hamiltonian path for every ordered pair of vertices, including (v, v):

h₂ : ∀ v₁ : V, ∀ v₂ : V,
  ∃ w : G.Walk v₁ v₂, w.IsHamiltonian

Mathlib's path condition forces a path from a vertex to itself to be the nil walk. Hamiltonicity then forces the graph to have at most one vertex. This contradicts the branch assumption n ≥ 4.

The checked proof in the companion file instantiates h₂ v v, rewrites the walk to nil, and lets omega close the contradiction. No lower-bound argument about edges occurs. A repaired Hamilton-connectedness premise must at least require v₁ ≠ v₂; the claimed inequality then needs a new proof.

B-05 is false under an adversarial Pow

The task introduces an unconstrained instance:

[Pow (G ⧸ N) ℤ]

Mathlib's IsCyclic is defined relative to the active integer-power operation. Take the nontrivial cyclic group Multiplicative (ZMod 2), quotient by the trivial subgroup, and define every integer power in the quotient to be 1. No power orbit can cover the nontrivial quotient. The companion file contains the complete Lean counterexample.

The arbitrary Pow binder should be removed, and the statement should use the canonical quotient group with the required normality assumption.

B-06 has a complete finite countermodel

Use:

R = ℤ
N = (4)
a = 2

Then a² = 4 ∈ N while a = 2 ∉ N. The quotient type ℤ ⧸ (4) has four elements. Transporting the field structure of GaloisField 2 2 across an arbitrary equivalence gives a literal DivisionRing (ℤ ⧸ (4)) instance. This transported multiplication is unrelated to canonical multiplication modulo four, but the task never requires compatibility.

The complete construction compiles in the companion file. Changing only [Ring R] to [CommRing R] leaves the countermodel intact. The mathematical requirement should be stated directly, for example [N.IsPrime] or [N.IsMaximal].

B-07 allows incompatible finite-field data

F, E, and K are sets in one ambient type, but their Field and Algebra structures are independent typeclass data. The inclusions F ⊆ E ⊆ K do not say that inclusion preserves either field operation, and they do not connect inclusion to the algebra maps.

A finite countermodel uses nested sets of cardinalities 2, 4, and 8, with field structures transported from GF(2), GF(4), and GF(8). The standard algebra structures from GF(2) to the other two fields satisfy the supplied base-extension assumptions, and GF(8)/GF(2) is normal. The conclusion would require an algebra structure from the four-element field to the eight-element field.

Such an algebra structure cannot exist. It would induce an injective group homomorphism from the 3-element unit group of GF(4) to the 7-element unit group of GF(8), contradicting Lagrange's theorem. The companion file machine-checks this no-algebra lemma for arbitrary fields of cardinalities 4 and 8. It does not yet encode the entire nested-set wrapper.

The statement should use IntermediateField for actual nested subfields, or explicitly provide a coherent [Algebra E K] [IsScalarTower F E K] together with compatibility between the inclusions and algebra maps.

C-05 is false with A = ∅

Take X = ℕ with its discrete topology, A = ∅, and Y = Set.univ. The empty set is compact and both subset assumptions hold, while the infinite discrete space Y is not compact. This counterexample is checked in the companion file.

If the intended theorem concerns closed subsets of compact sets, the premise should be Y ⊆ A ∧ IsClosed Y.

D-02 fails on a disconnected domain

Let S = ℝ \ {0} and define f to be zero on the negative component and one on the positive component. At every point of S, f is locally constant relative to S, so its within-derivative is zero and uniformly bounded. Nevertheless, the pairs -1/n and 1/n approach one another while their function values remain one unit apart. Thus f is not uniformly continuous on S.

The standard repair is to add a connected geometric condition such as Convex ℝ S, which supports a mean-value or Lipschitz argument. This countermodel is supplied here as a mathematical argument; a complete Lean encoding is not claimed in the companion file.

D-03 fails on a degenerate interval

Set a = b = 0 and f ≡ 1. The interval integral is zero, but Icc 0 0 contains zero and f 0 ≠ 0. The complete Lean counterexample is in the companion file.

Adding a < b gives the conventional nondegenerate statement. The weaker a ≠ b is logically sufficient for the literal conclusion because Icc a b is empty when b < a.

D-07 has no finite p-th-moment hypothesis

The declaration contains two binders named X. Elaboration shows that the first explicit binder is unused and the later implicit X occurs in h₂, h₃, and the conclusion. The duplicate name is confusing but is not itself the counterexample.

The decisive premise is:

h₃ : ∃ M : ℝ, 𝔼[fun ω => |X ω| ^ p] = M

It is true for every X and p:

exact ⟨𝔼[fun ω => |X ω| ^ p], rfl⟩

The companion file checks this fact. The remaining substantive hypothesis is only first-moment integrability. A Pareto variable with tail exponent 3/2 and p = 2 has finite first moment, while x² P(X > x) = x^(1/2) for x ≥ 1, so the claimed limit fails. The Pareto construction is a mathematical countermodel and is not fully formalized in the companion file.

The intended true hypothesis is Integrable (fun ω => |X ω| ^ p). Under it, the desired tail limit follows from tail truncation. The duplicate binder should also be removed.

E-01 is unsupported as an executable benchmark task

E-01 asks for an ordinary definition of:

Decidable (∃ a b c d : ℤ,
  n = a ^ 3 + b ^ 3 + c ^ 3 + d ^ 3)

The universal four-cubes conjecture remains open. A recent survey states that it is believed every integer is a sum of four integer cubes: James Maynard, Sums of three positive cubes, 2026. This does not prove that the pointwise membership predicate is undecidable, so no undecidability claim is made here.

The benchmark problem is sharper. ScienceBoard supplies no reference total decider or verified search bound, while the current Raw and VM evaluators both accept classical noncomputable completion. E-01 therefore cannot establish either discovery of a genuine algorithm or proof of the open universal conjecture.

It should remain quarantined until the maintainers provide an independent reference implementation under a verifier that enforces the intended computability requirement.

E-02 specializes to deciding Nonempty α

Choose the ideal arising from the principal filter on Set.univ; this gives I = {∅}. Any A ⊆ I satisfying inter_family A must be the empty family, because a family containing ∅ fails its own nonempty-intersection condition. For A = ∅, star A says that the intersection of the empty family, Set.univ, is nonempty. The maximal-cardinality condition is automatic because the empty family is the only admissible family.

The target proposition therefore specializes to Nonempty α. A uniform executable E-02 implementation would decide Nonempty α for every arbitrary opaque type α, which is not a computable operation in this representation.

Changing the declaration to noncomputable def would make it a valid classical specification, but would not repair it as an executable benchmark. A genuine algorithmic version needs finite, enumerable, decidable data, for example a Fintype/DecidableEq carrier and finite representations such as Finset (Finset α) instead of unrestricted higher-order Set inputs.

Requested actions

1. Quarantine the nine false theorem tasks until corrected:

   A-02, A-04, B-05, B-06, B-07,
   C-05, D-02, D-03, D-07
   

2. Rewrite B-01 and B-02 according to their intended mathematics and regenerate their reference trajectories.

3. Quarantine E-01 pending a reference total decider and an evaluator that checks the intended computability property.

4. Redesign E-02 with finite, enumerable, decidable input representations if it is intended to remain algorithmic.

5. Identify published score tables that included any affected Raw or VM JSON configurations and recompute those aggregates after curation.

6. Add an offline validation gate before a Lean task enters the scored set. It should record the elaborated declaration type, an independent reference proof or program, exact Lean and Mathlib commits, boundary tests, and adversarial typeclass-instance tests.

7. Optionally add a manually adjudicated invalid-task report channel. This can help future audits, but it is not a substitute for task curation and should not be treated as the only repair.

Useful evidence categories for offline review include:

false_statement
elaboration_mismatch
noncomputable_generalization
specification_mismatch
unsupported_open_task

Suggested repair directions

Task	Suggested direction
A-02	Exclude both boundary cases for any strict version, or investigate ≤; verify the new statement independently
A-04	Replace ℵ with ℵ₀
B-01	Replace IsCoprime with Nat.Coprime
B-02	Require distinct endpoints and re-prove the edge bound
B-05	Remove arbitrary Pow; use the canonical quotient group
B-06	State [N.IsPrime] or [N.IsMaximal] directly
B-07	Use IntermediateField or a coherent scalar tower
C-05	Use Y ⊆ A ∧ IsClosed Y if that is the intended theorem
D-02	Add convexity or another suitable domain condition
D-03	Add a < b
D-07	Require actual p-th-moment integrability and remove the duplicate binder
E-01	Quarantine pending a reference total decider and computability-enforcing evaluation
E-02	Replace unrestricted sets with finite decidable representations

References

• ScienceBoard Lean Raw tasks at the audited commit
• ScienceBoard Lean VM tasks at the audited commit
• Mathlib IsCyclic and the active Pow instance
• Mathlib ideal quotient definitions
• Maynard's 2026 survey discussing the four-cubes conjecture