diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index cfe5764..99b1eed 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -44,6 +44,7 @@ harmonic_geometric_arithmetic₂
 harmonic_geometric_arithmetic₃
 mantel
 fundamental_theorem_of_algebra
+Matrix.permanent_conjecture
 chapter28.pigeon_hole_principle
 chapter28.handshaking
 chapter44.friendship_theorem
diff --git a/blueprint/src/chapter/chapter24.tex b/blueprint/src/chapter/chapter24.tex
index 1fb6c60..922a773 100644
--- a/blueprint/src/chapter/chapter24.tex
+++ b/blueprint/src/chapter/chapter24.tex
@@ -2,6 +2,7 @@ \chapter{Van der Waerden's permanent conjecture}
 
 \begin{theorem}
   \label{vanderwaerden}
+  \lean{Matrix.permanent_conjecture}
   Let $M = (m_{ij})$ be a doubly stochastic $n \times n$ matrix.
   Then
   \[\per M \ge \frac{n!}{n^n}\]