lean_workbook_plus_38580

⚠️ 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.

There are $1296$ possible results (note that order matters), all equally likely. Take the first die's throw, then either the other three all need to be the same as each other ( $6$ possibilities for the first die, then $6$ for the rest, giving $6\cdot6=36$ possibilities) or exactly two of them are the same as the first ( $6$ possibilities for the first roll, $3$ possibilities for which die has the non-identical roll, and $5$ for the result of that die, giving $6\cdot3\cdot5=90$ possibilities). This gives a probability of $\frac{126}{1296}=\frac{7}{72}$ .

Why this node was retired

The posted statement is

theorem lean_workbook_plus_38580 :
  (36 + 90) / 1296 = 7 / 72   :=  by sorry

The probability reduction is checked in ℕ, so both quotients are zero; no probability model or rational count is certified by that equality.

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

Prove (36+90)/1296=7/72 in ℚ. For the dice claim, use the uniform sample space {1,…,6}⁴ and prove that at least three matching dice occur in exactly126 outcomes, hence probability7/72.

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.