lean_workbook_plus_21024

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

Let $X$ be the random variable equal to sum of all the scores on the $n$ dice. Now it is easy to show that $\text{P}(X = k) = \text{P}(X = 7n - k)$ for any positive integer $k$ . So if $\text{P}(X = 1994) = \text{P}(X = S)$ then $S = 7n - 1994$ and we know that $n \geq 333$ . So $S \geq 7 \times 333 - 1994 = 337$ .

Why this node was retired

The posted statement is

theorem lean_workbook_plus_21024  (n S : ℕ)
  (h₀ : 0 < n ∧ 0 < S)
  (h₁ : 1994 ≤ S)
  (h₂ : S ≤ 7 * n)
  (h₃ : ∀ k, 0 < k → Nat.Prime k → Nat.Prime (S - k)) :
  S = 337   :=  by sorry

An unrelated impossible prime-reflection hypothesis replaced dice probabilities. A prime k>S gives S−k=0, and the inserted conclusion337 also contradicts S≥1994.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

Define the sum X of n independent fair six-sided dice and prove P(X=k)=P(X=7n−k). Recover additional conditions on the second equal-probability value S before claiming S=7n−1994 or an extremum; symmetry alone does not rule out S=1994 or zero-probability ties.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.