Enumerative combinatorics · formal theorem
For every finite Young diagram, multiplying all hook lengths by the number of standard Young tableaux gives the factorial of the number of cells.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
The theorem at a glance
Accessible transcript
f^μ · ∏ h(c) = |μ|!
The exact multiplicative Hook-Length Formula, its local hook statistic, tableau count, and induction architecture are gathered in one reference.
COMBINATORICS · YOUNG DIAGRAMS
HOOK-LENGTH FORMULA
LOCAL HOOKS CONTROL EVERY STANDARD TABLEAU
FOR EVERY FINITE YOUNG DIAGRAM μ
f^μ · ∏ h(c) = |μ|!
h(c) counts c, the cells to its right, and the cells below it.
f^μ counts standard tableaux of shape μ.
THE FAMILIAR FORM
f^μ = |μ|! / ∏ h(c)
HOW THE PROOF MOVES
REMOVE THE MAXIMUM CORNER · COMPARE HOOK PRODUCTS · REWRITE WITH CONTENTS · EVALUATE THE CONTENT SUM · CLOSE BY STRONG INDUCTION
EXACT SCOPE
Finite Young diagrams, including the empty diagram.
Theorem schematic
Proof architecture
Follow the retained proof from removable corners through hook-product ratios and finite interpolation to the strong-induction close.
These source-anchored stages explain the retained proof route. They are not an extracted Lean proof-term dependency graph.
f^μ = ∑ f^(μ\c)
The largest tableau entry must occupy a removable corner, so every standard tableau belongs to exactly one smaller-shape branch.
CellhookCellshookLengthIsStandardTableaustandardTableauCounthookProducthookLengthFormula
(4,3,2) → (3,3,2)
Deleting the top-right corner of the (4,3,2) example leaves (3,3,2); only hooks whose arms crossed that corner change.
CellhookCellshookLengthIsStandardTableaustandardTableauCounthookProducthookLengthFormula
The ratio between the original and corner-deleted hook products factors along one row and one column, then telescopes into addable and removable contents.
CellhookCellshookLengthIsStandardTableaustandardTableauCounthookProducthookLengthFormula
After rewriting every corner branch by contents, the required hook-product identity reduces to a finite rational sum over removable corners.
CellhookCellshookLengthIsStandardTableaustandardTableauCounthookProducthookLengthFormula
A finite interpolation identity evaluates the content sum, supplying exactly the scalar needed to balance the branching recurrence.
CellhookCellshookLengthIsStandardTableaustandardTableauCounthookProducthookLengthFormula
Strong induction substitutes the formula for every erased-corner child. In the (4,3,2) example there are three such children. The branching identity supplies the missing factor, and the empty diagram anchors the base case.
CellhookCellshookLengthIsStandardTableaustandardTableauCounthookProducthookLengthFormulaExact formal proposition
theorem hookLengthFormula : HookLengthFormulaStatementResult boundary
For every finite Young diagram μ, hookProduct μ · standardTableauCount μ = (μ.card)!.
These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.
Continue the mathematics
The pinned theorem and its complete local import closure let internal and external agents inspect the proof, compare an alternate route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks every proposed extension against its exact formal statement.
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and an agent continuation file. Mathlib and other third-party dependencies are not bundled.
Independent publication review
Lean checks the proof. Independent AI review separately accepted evidence completeness, statement alignment, result boundary, and the retained theorem wording. Those gates apply to the formal result; generated media is reviewed and promoted separately. Neither review replaces Lean's proof check or broadens the theorem.
Independent review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.
The formal declaration was accepted against the named theorem and its exact variant.
The accepted boundary keeps nearby stronger or commonly confused claims out of scope.
Independent review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.
The first-party source link is pinned to the checked package commit and exact Lean file.
A validated accepted-result record binds the four reviews to the checked formalization.