diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
index 1d7e915..cdbf343 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@@ -623,7 +623,8 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ)  : Pa' f = Pa' f' ↔ f =
   intro h
   rw [h]
 
-/-- A helper function for what follows. TODO: replace this with mathlib functions. -/
+/-! TODO: Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`. -/
+/-- A helper function for what follows. -/
 def join (g : Fin n.succ → ℚ) (f : Fin n → ℚ) :  (Fin n.succ) ⊕ (Fin n) → ℚ := fun i =>
   match i with
   | .inl i => g i
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
index c7dc70e..5af2a8e 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -608,7 +608,8 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ)  : Pa' f = Pa' f' 
   intro h
   rw [h]
 
-/-- A helper function for what follows. TODO: replace this with mathlib functions. -/
+/-! TODO: Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`. -/
+/-- A helper function for what follows. -/
 def join (g f : Fin n → ℚ) :  Fin n ⊕ Fin n → ℚ := fun i =>
   match i with
   | .inl i => g i
diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
index c585e5c..b20fb59 100644
--- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -106,7 +106,8 @@ lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols)
     ((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by
   rfl
 
-/-- The permutation which swaps i and j. TODO: Replace with: `Equiv.swap`. -/
+/-! TODO: Replace the definition of `pairSwap` with `Equiv.swap`. -/
+/-- The permutation which swaps i and j. -/
 def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where
   toFun s :=
     if s = i then
diff --git a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
index 2eed792..d0d9ce0 100644
--- a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
+++ b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
@@ -10,11 +10,8 @@ import Mathlib.Logic.Equiv.Fin
 
 For the `n`-even case we define the property of a charge assignment being vector like.
 
-## TODO
-
-The `n`-odd case.
-
 -/
+/-! TODO: Define vector like ACC in the `n`-odd case. -/
 universe v u
 
 open Nat
diff --git a/HepLean/Mathematics/LinearMaps.lean b/HepLean/Mathematics/LinearMaps.lean
index d56b6e7..d6dbf02 100644
--- a/HepLean/Mathematics/LinearMaps.lean
+++ b/HepLean/Mathematics/LinearMaps.lean
@@ -12,12 +12,8 @@ import Mathlib.Data.Fintype.BigOperators
 Some definitions and properties of linear, bilinear, and trilinear maps, along with homogeneous
 quadratic and cubic equations.
 
-## TODO
-
-Use definitions in `Mathlib4` for definitions where possible.
-In particular a HomogeneousQuadratic should be a map `V →ₗ[ℚ] V →ₗ[ℚ] ℚ`  etc.
-
 -/
+/-! TODO: Replace the definitions in this file with Mathlib definitions. -/
 
 /-- The structure defining a homogeneous quadratic equation. -/
 @[simp]
diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
index 1618fb0..a79f0db 100644
--- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
@@ -16,17 +16,13 @@ a four velocity `u` to a four velocity `v`.
 
 A boost is the special case of a generalised boost when `u = stdBasis 0`.
 
-## TODO
-
-- Show that generalised boosts are in the restricted Lorentz group.
-- Define boosts.
-
 ## References
 
 - The main argument follows: Guillem Cobos, The Lorentz Group, 2015:
   https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
 
 -/
+/-! TODO: Show that generalised boosts are in the restricted Lorentz group. -/
 noncomputable section
 
 namespace LorentzGroup
diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
index 6ef2e6b..be1963c 100644
--- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
@@ -11,11 +11,8 @@ import HepLean.SpaceTime.LorentzGroup.Proper
 We define the give a series of lemmas related to the orthochronous property of lorentz
 matrices.
 
-## TODO
-
-- Prove topological properties.
-
 -/
+/-! TODO: Prove topological properties of the Orthochronous Lorentz Group. -/
 
 noncomputable section
 
diff --git a/HepLean/StandardModel/Basic.lean b/HepLean/StandardModel/Basic.lean
index 9d954fa..f145c99 100644
--- a/HepLean/StandardModel/Basic.lean
+++ b/HepLean/StandardModel/Basic.lean
@@ -21,7 +21,7 @@ open Matrix
 open Complex
 open ComplexConjugate
 
-/-- The global gauge group of the standard model. TODO: Generalize to quotient. -/
+/-- The global gauge group of the standard model. -/
 abbrev GaugeGroup : Type :=
   specialUnitaryGroup (Fin 3) ℂ × specialUnitaryGroup (Fin 2) ℂ × unitary ℂ
 
diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean
index d9ad6c8..f87843c 100644
--- a/HepLean/StandardModel/HiggsBoson/Basic.lean
+++ b/HepLean/StandardModel/HiggsBoson/Basic.lean
@@ -41,7 +41,8 @@ open SpaceTime
 
 -/
 
-/-- The trivial vector bundle 𝓡² × ℂ². (TODO: Make associated bundle.) -/
+/-! TODO: Make `HiggsBundle` an associated bundle. -/
+/-- The trivial vector bundle 𝓡² × ℂ². -/
 abbrev HiggsBundle := Bundle.Trivial SpaceTime HiggsVec
 
 instance : SmoothVectorBundle HiggsVec HiggsBundle SpaceTime.asSmoothManifold  :=