lean_workbook_plus_74623

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

Find the number of $n\times n$ matrices filled with nonnegative integers such that every row and every column have sum equal to $r$.

Why this node was retired

The posted statement is

theorem lean_workbook_plus_74623 (n r : ℕ) : ∃ R: Fin n → Fin n → ℕ, (∀ i, ∑ j, R i j = r) ∧ (∀ j, ∑ i, R i j = r)   :=  by sorry

The diagonal witness proves existence only; the source asks to count every allowed matrix. No closed counting answer is inferred from this proof.

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

Ask for the cardinality of the finite set of n×n matrices with entries in{0,…,r} and all row and column sums r, rather than mere existence.

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.