diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean
index 608b3c2df318c7..8c4edf0c1247f3 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean
@@ -22,6 +22,10 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
 * T_n(x) ∈ [-1, 1] iff x ∈ [-1, 1]: `abs_eval_T_real_le_one_iff`
 * Zeroes of T and U: `roots_T_real`, `roots_U_real`
 * Local extrema of T: `isLocalExtr_T_real_iff`, `isExtrOn_T_real_iff`
+
+## TODO
+
+Prove that the roots of the Chebyshev polynomials (except 0) are irrational.
 -/
 
 public section
diff --git a/Mathlib/RingTheory/Polynomial/Chebyshev.lean b/Mathlib/RingTheory/Polynomial/Chebyshev.lean
index a5976b559aa429..5a164fe2757426 100644
--- a/Mathlib/RingTheory/Polynomial/Chebyshev.lean
+++ b/Mathlib/RingTheory/Polynomial/Chebyshev.lean
@@ -54,8 +54,6 @@ and do not have `map (Int.castRingHom R)` interfering all the time.
 
 * Redefine and/or relate the definition of Chebyshev polynomials to `LinearRecurrence`.
 * Add explicit formula involving square roots for Chebyshev polynomials
-* Compute zeroes and extrema of Chebyshev polynomials.
-* Prove that the roots of the Chebyshev polynomials (except 0) are irrational.
 -/
 
 @[expose] public section