diff --git a/blueprint/src/chapter/reductions.tex b/blueprint/src/chapter/reductions.tex index 8daf86d2..4b85017c 100644 --- a/blueprint/src/chapter/reductions.tex +++ b/blueprint/src/chapter/reductions.tex @@ -21,7 +21,8 @@ \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime} Euler proved Fermat's Last Theorem for $p=3$; at the time of writing this is not in mathlib. \begin{lemma}\label{p_not_three}\lean{FLT.fermatLastTheoremThree}\leanok -\discussion{16} +%%\discussion{16} +{\bf TODO} discussion. There are no nontrivial solutions in integers to $a^3+b^3=c^3$. \end{lemma} \begin{proof}