diff --git a/blueprint/src/chapter/ch02reductions.tex b/blueprint/src/chapter/ch02reductions.tex
index 1a8f5c28..16324965 100644
--- a/blueprint/src/chapter/ch02reductions.tex
+++ b/blueprint/src/chapter/ch02reductions.tex
@@ -28,7 +28,7 @@ \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime}
   There are no solutions in positive integers to $a^3+b^3=c^3$.
 \end{lemma}
 \begin{proof}
-  The proof has been formalised in Lean in the FLT-regular project \href{https://github.com/leanprover-community/flt-regular/blob/861b7df057140b45b8bb7d30d33426ffbbdda52b/FltRegular/FltThree/FltThree.lean#L698}{\underline{here}}. To get this node green, the proof (or another proof) needs to be upstreamed to mathlib.
+  The proof has been formalised in Lean in the FLT-regular project \href{https://github.com/leanprover-community/flt-regular/blob/861b7df057140b45b8bb7d30d33426ffbbdda52b/FltRegular/FltThree/FltThree.lean#L698}{\underline{here}}. To get this node green, the proof (or another proof) needs to be upstreamed to mathlib. This is currently work in progress by a team from the Lean For the Curious Mathematician conference held in Luminy in March 2024.
 \end{proof}
 
 \begin{corollary}\label{p_ge_5_counterexample_of_not_FermatLastTheorem}\lean{p_ge_5_counterexample_of_not_FermatLastTheorem}\leanok If there is a counterexample to Fermat's Last Theorem, then there is a counterexample $a^p+b^p=c^p$ with $p$ prime and $p\geq 5$.