ProofAtlas

Enumerative combinatorics · formal theorem

Hook-Length Formula

For every finite Young diagram, multiplying all hook lengths by the number of standard Young tableaux gives the factorial of the number of cells.

Scope: For every finite Young diagram μ, hookProduct μ · standardTableauCount μ = (μ.card)!.

Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Hook-length formula statement mapA finite Young diagram links its hook-length product, its standard tableaux, and the factorial of its number of cells through one exact multiplicative identity.
Exact scope: For every finite Young diagram μ, hookProduct μ · standardTableauCount μ = (μ.card)!.

Exact formal proposition

Hypotheses and conclusion

This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.

def HookLengthFormulaStatement : Prop :=
  ∀ μ : YoungDiagram,
    hookProduct μ * standardTableauCount μ = Nat.factorial μ.card
Definitions used in this proposition

standardTableauCount

noncomputable def standardTableauCount (μ : YoungDiagram) : ℕ :=
  Fintype.card {T : Cell μ → Fin μ.card // IsStandardTableau μ T}

hookProduct

def hookProduct (μ : YoungDiagram) : ℕ :=
  μ.cells.attach.prod fun c ↦ hookLength μ c
Lean wrapper declaration

The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.

theorem hookLengthFormula : HookLengthFormulaStatement
Open main Lean file

Proof route

How the Hook-Length Formula is proved

6 proof stages

Follow the retained proof from removable corners through hook-product ratios and finite interpolation to the strong-induction close.

These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.

  1. The left-justified Young diagram with row lengths 4, 3, and 1 has its three removable corners highlighted, with arrows to the three seven-cell diagrams obtained by deleting one corner.
    Removing the maximum entry from any removable corner partitions the standard tableaux into three smaller-shape branches in this example.
    01

    Tableaux branch at a removable corner

    f^μ = ∑ f^(μ\c)

    The Hook Length proof-stage figure uses the concrete partition (4,3,1). Its removable corners lead exactly to the child partitions (3,3,1), (4,2,1), and (4,3), illustrating the tableau-count recurrence without claiming this single example proves the general identity.

    Lean lemmas for this step
    • Cell
    • hookCells
    • hookLength
    • IsStandardTableau
    • standardTableauCount
    • hookProduct
    • hookLengthFormula
  2. Scientific figure illustrating: A single corner deletion isolates the hooks that lose one cell.
    A single corner deletion isolates the hooks that lose one cell.
    02

    Only crossing hooks change

    (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.

    Lean lemmas for this step
    • Cell
    • hookCells
    • hookLength
    • IsStandardTableau
    • standardTableauCount
    • hookProduct
    • hookLengthFormula
  3. Scientific figure illustrating: Row and column hook changes telescope into content factors.
    Row and column hook changes telescope into content factors.
    03

    Hook ratios become content intervals

    The ratio between the original and corner-deleted hook products factors along one row and one column, then telescopes into addable and removable contents.

    Lean lemmas for this step
    • Cell
    • hookCells
    • hookLength
    • IsStandardTableau
    • standardTableauCount
    • hookProduct
    • hookLengthFormula
  4. A Young diagram with row lengths three and two highlights its two removable corners, with separate arrows to the child shapes with row lengths two and two, and three and one.
    Deleting either removable corner of the (3,2) diagram gives one of two one-cell-smaller shapes.
    04

    Two removable corners give two smaller shapes

    The scientific figure shows the parent Young diagram (3,2), highlights the corners at row 1 column 3 and row 2 column 2, and maps them separately to the one-cell deletions (2,2) and (3,1).

    Lean lemmas for this step
    • Cell
    • hookCells
    • hookLength
    • IsStandardTableau
    • standardTableauCount
    • hookProduct
    • hookLengthFormula
  5. A valid left-justified Young diagram with rows of three and two cells marks two removable corners and three addable positions, which become five interlaced content nodes and resolve into the same five-cell gold silhouette.
    Two removable contents and three addable contents interlace in the finite interpolation step, resolving the branching sum into the diagram’s five-cell cardinality.
    05

    Finite interpolation resolves the content sum

    At left, a valid English-convention Young diagram has weakly decreasing row lengths 3 and 2, with two emerald removable corners and three cobalt outlined addable positions. In the center, the corresponding five content nodes alternate addable-removable-addable-removable-addable and are linked only by adjacent discrete arches. A transformation arrow leads to five gold cells in the same 3,2 silhouette, representing the diagram cardinality without an in-raster equation.

    Lean lemmas for this step
    • Cell
    • hookCells
    • hookLength
    • IsStandardTableau
    • standardTableauCount
    • hookProduct
    • hookLengthFormula
  6. A nine-cell Young diagram with rows of four, three, and two branches to three eight-cell diagrams with row lengths three-three-two, four-two-two, and four-three-one; dashed gold ghosts mark the deleted corner in each child.
    Deleting each removable corner of the (4,3,2) Young diagram gives exactly the three children (3,3,2), (4,2,2), and (4,3,1) used in the induction step.
    06

    Three removable corners give exactly three induction children

    A left-justified nine-cell Young diagram has four cells in its top row, three in its middle row, and two in its bottom row. Three gold-marked removable corners branch to three eight-cell children. The left child has row lengths (3,3,2) and a dashed removed-cell ghost at row 1 column 4. The middle child has row lengths (4,2,2) and a dashed ghost at row 2 column 3. The right child has row lengths (4,3,1) and a dashed ghost at row 3 column 2. Emerald curves gather the three valid smaller shapes into one quiet induction-closure motif.

    Lean lemmas for this step
    • Cell
    • hookCells
    • hookLength
    • IsStandardTableau
    • standardTableauCount
    • hookProduct
    • hookLengthFormula

The theorem at a glance

Hook-Length Formula at a glance

Local hook sizes determine the number of all standard tableaux of a finite Young diagram.
Local hook sizes determine the number of all standard tableaux of a finite Young diagram.

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.

Read the complete poster transcript

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

Hooks turn local geometry into a global count

Scientific figure illustrating: A Young diagram links one local hook to the global tableau-count identity.
A Young diagram links one local hook to the global tableau-count identity.

f^μ · ∏ h(c) = |μ|!

A finite Young diagram assigns each cell a hook extending rightward and downward; multiplying those local hook lengths controls the total number of standard tableaux.

Result boundary

What this theorem does—and does not—establish

For every finite Young diagram μ, hookProduct μ · standardTableauCount μ = (μ.card)!.

About these visual explanations

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.

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.

Continue the mathematics

Open questions and extensions

The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.

What the source ZIP contains

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.

Complete checked Lean source · 1 Lean file · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Publication review

Review record

Publication reviews accepted

Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.

01

Formal evidence

The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.

02

Statement alignment

The formal declaration was accepted against the named theorem and its exact variant.

03

Result boundary

The accepted boundary keeps nearby stronger or commonly confused claims out of scope.

04

Public wording

The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.

05

Canonical source

The first-party source link is pinned to the checked package commit and exact Lean file.

06

Accepted result

A validated accepted-result record binds the four reviews to the checked formalization.

Expanded visual

Open original image