diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index 68a7426..451f47d 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -119,7 +119,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
     apply LinSols.ext
     exact χ.chargesAddCommMonoid.nsmul_succ _ _
 
-/-- An instance providing the operations and properties for `LinSols` to form an
+/-- An instance providing the operations and properties for `LinSols` to form a
   module over `ℚ`. -/
 @[simps!]
 instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
@@ -147,7 +147,7 @@ instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
     exact χ.chargesModule.add_smul _ _ _
 
 /-- An instance providing the operations and properties for `LinSols` to form an
-  an additive community. -/
+  additive commutative group. -/
 instance linSolsAddCommGroup (χ : ACCSystemLinear) : AddCommGroup χ.LinSols :=
   Module.addCommMonoidToAddCommGroup ℚ
 
@@ -201,8 +201,8 @@ def quadSolsInclLinSols (χ : ACCSystemQuad) : χ.QuadSols →[ℚ] χ.LinSols w
   toFun := QuadSols.toLinSols
   map_smul' _ _ := rfl
 
-/-- If there are no quadratic equations (i.e. no U(1)'s in the underlying gauge group. The inclusion
-  of linear solutions into quadratic solutions. -/
+/-- The inclusion of the linear solutions into the quadratic solutions, where there is
+  no quadratic equations (i.e. no U(1)'s in the underlying gauge group). -/
 def linSolsInclQuadSolsZero (χ : ACCSystemQuad) (h : χ.numberQuadratic = 0) :
     χ.LinSols →[ℚ] χ.QuadSols where
   toFun S := ⟨S, by intro i; rw [h] at i; exact Fin.elim0 i⟩
@@ -233,7 +233,7 @@ lemma Sols.ext {χ : ACCSystem} {S T : χ.Sols} (h : S.val = T.val) :
   cases' S
   simp_all only
 
-/-- We say a charge S is a solution if it extends to a solution. -/
+/-- A charge `S` is a solution if it extends to a solution. -/
 def IsSolution (χ : ACCSystem) (S : χ.Charges) : Prop :=
  ∃ (sol : χ.Sols), sol.val = S
 
diff --git a/HepLean/AnomalyCancellation/GroupActions.lean b/HepLean/AnomalyCancellation/GroupActions.lean
index d9b21fc..05edfa9 100644
--- a/HepLean/AnomalyCancellation/GroupActions.lean
+++ b/HepLean/AnomalyCancellation/GroupActions.lean
@@ -18,13 +18,13 @@ From this we define
 
 -/
 
-/-- The type of of a group action on a system of charges is defined as a representation on
+/-- The type of a group action on a system of charges is defined as a representation on
 the vector spaces of charges under which the anomaly equations are invariant.
 -/
 structure ACCSystemGroupAction (χ : ACCSystem) where
   /-- The underlying type of the group. -/
   group : Type
-  /-- An instance given group the structure of a group. -/
+  /-- An instance given the `group` component the structure of a `Group`. -/
   groupInst : Group group
   /-- The representation of group acting on the vector space of charges. -/
   rep : Representation ℚ group χ.Charges
@@ -79,8 +79,7 @@ lemma rep_linSolRep_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g :
     (S : χ.LinSols) : χ.linSolsIncl (G.linSolRep g S) =
     G.rep g (χ.linSolsIncl S) := rfl
 
-/-- An instance given the structure to define a multiplicative action of `G.group` on `quadSols`.
- -/
+/-- A multiplicative action of `G.group` on `quadSols`. -/
 instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
     MulAction G.group χ.QuadSols where
   smul f S := ⟨G.linSolRep f S.1, by
@@ -112,8 +111,7 @@ instance solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.
   smul g S := ⟨G.quadSolAction.toFun S.1 g, by
    simp only [MulAction.toFun_apply]
    change χ.cubicACC (G.rep g S.val) = 0
-   rw [G.cubicInvariant, S.cubicSol]
-  ⟩
+   rw [G.cubicInvariant, S.cubicSol]⟩
   mul_smul f1 f2 S := by
     apply ACCSystem.Sols.ext
     change (G.rep.toFun (f1 * f2)) S.val = _
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index 3623350..6774b88 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@@ -48,7 +48,7 @@ def LineEqPropSol (R : MSSMACC.Sols) : Prop :=
   cubeTriLin R.val R.val Y₃.val * quadBiLin B₃.val R.val -
   cubeTriLin R.val R.val B₃.val * quadBiLin Y₃.val R.val = 0
 
-/-- A rational which appears in `toSolNS` acting on sols, and which been zero is
+/-- A rational which appears in `toSolNS` acting on sols, and which being zero is
 equivalent to satisfying `lineEqPropSol`. -/
 def lineEqCoeff (T : MSSMACC.Sols) : ℚ := dot Y₃.val B₃.val * α₃ (proj T.1.1)
 
@@ -185,30 +185,30 @@ lemma inCubeSolProp_iff_proj_inCubeProp (R : MSSMACC.Sols) :
 `lineEqProp`. -/
 def InLineEq : Type := {R : MSSMACC.AnomalyFreePerp // LineEqProp R}
 
-/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition
+/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the conditions
 `lineEqProp` and `inQuadProp`. -/
 def InQuad : Type := {R : InLineEq // InQuadProp R.val}
 
-/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition
+/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the conditions
 `lineEqProp`, `inQuadProp` and `inCubeProp`. -/
 def InQuadCube : Type := {R : InQuad // InCubeProp R.val.val}
 
 /-- Those solutions which do not satisfy the condition `lineEqPropSol`. -/
 def NotInLineEqSol : Type := {R : MSSMACC.Sols // ¬ LineEqPropSol R}
 
-/-- Those solutions which satisfy the condition `lineEqPropSol` by not `inQuadSolProp`. -/
+/-- Those solutions which satisfy the condition `lineEqPropSol` but not `inQuadSolProp`. -/
 def InLineEqSol : Type := {R : MSSMACC.Sols // LineEqPropSol R ∧ ¬ InQuadSolProp R}
 
 /-- Those solutions which satisfy the condition `lineEqPropSol` and `inQuadSolProp` but
 not `inCubeSolProp`. -/
 def InQuadSol : Type := {R : MSSMACC.Sols // LineEqPropSol R ∧ InQuadSolProp R ∧ ¬ InCubeSolProp R}
 
-/-- Those solutions which satisfy the condition all the conditions `lineEqPropSol`, `inQuadSolProp`
+/-- Those solutions which satisfy the conditions `lineEqPropSol`, `inQuadSolProp`
 and `inCubeSolProp`. -/
 def InQuadCubeSol : Type :=
   {R : MSSMACC.Sols // LineEqPropSol R ∧ InQuadSolProp R ∧ InCubeSolProp R}
 
-/-- Given a `R` perpendicular to `Y₃` and `B₃` a quadratic solution. -/
+/-- Given an `R` perpendicular to `Y₃` and `B₃` a quadratic solution. -/
 def toSolNSQuad (R : MSSMACC.AnomalyFreePerp) : MSSMACC.QuadSols :=
   lineQuad R
     (3 * cubeTriLin R.val R.val Y₃.val)
@@ -230,7 +230,7 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) :
   ring_nf
   simp
 
-/-- Given a `R ` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
+/-- Given an `R` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
 not surjective. -/
 def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) =>
   a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R)
@@ -258,7 +258,7 @@ lemma toSolNS_proj (T : NotInLineEqSol) : toSolNS (toSolNSProj T.val) = T.val :=
   rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h1]
   simp
 
-/-- Given a element of `inLineEq × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
+/-- A solution to the ACCs, given an element of `inLineEq × ℚ × ℚ × ℚ`. -/
 def inLineEqToSol : InLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, c₁, c₂, c₃) =>
   AnomalyFreeMk'' (lineQuad R.val c₁ c₂ c₃)
     (by
@@ -301,7 +301,7 @@ lemma inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
   rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2]
   simp
 
-/-- Given a element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
+/-- Given an element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
 def inQuadToSol : InQuad × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a₁, a₂, a₃) =>
   AnomalyFreeMk' (lineCube R.val.val a₁ a₂ a₃)
     (by
@@ -389,7 +389,7 @@ lemma inQuadCubeToSol_proj (T : InQuadCubeSol) :
   rw [show dot Y₃.val B₃.val = 108 by rfl]
   simp
 
-/-- Given an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` a solution. We will
+/-- A solution from an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ`. We will
 show that this map is a surjection. -/
 def toSol : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, b, c) =>
   if h₃ : LineEqProp R ∧ InQuadProp R ∧ InCubeProp R then
diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
index 4a2ed22..1371ee9 100644
--- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
+++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
@@ -136,7 +136,7 @@ lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
   rw [boundary_castSucc hS hk, boundary_succ hS hk]
   ring
 
-/-- We say a `S ∈ charges` has a boundary if there exists a `k ∈ Fin n` which is a boundary. -/
+/-- A `S ∈ charges` has a boundary if there exists a `k ∈ Fin n` which is a boundary. -/
 @[simp]
 def HasBoundary (S : (PureU1 n.succ).Charges) : Prop :=
   ∃ (k : Fin n), Boundary S k
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
index 986f65a..24686eb 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@@ -667,7 +667,7 @@ lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) =
   simp only [Fintype.card_sum, Fintype.card_fin, mul_eq]
   omega
 
-/-- The basis formed out of our basisa vectors. -/
+/-- The basis formed out of our `basisa` vectors. -/
 noncomputable def basisaAsBasis :
     Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols :=
   basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
index 9b9f6b3..064c3d3 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@@ -67,7 +67,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic
   linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
    (lineInCubic_expand h g f hS 1 2) / 6
 
-/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
+/-- A `LinSol` satisfies `LineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
 def LineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
   ∀ (M : (FamilyPermutations (2 * n.succ)).group),
   LineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S)
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
index c01a557..edd2003 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@@ -61,16 +61,16 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S
   linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
      (lineInCubic_expand h g f hS 1 2) / 6
 
-/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
+/-- A `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
 def LineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
   ∀ (M : (FamilyPermutations (2 * n + 1)).group),
     LineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S)
 
-/-- If `lineInCubicPerm S` then `lineInCubic S`. -/
+/-- If `lineInCubicPerm S`, then `lineInCubic S`. -/
 lemma lineInCubicPerm_self {S : (PureU1 (2 * n + 1)).LinSols} (hS : LineInCubicPerm S) :
     LineInCubic S := hS 1
 
-/-- If `lineInCubicPerm S` then `lineInCubicPerm (M S)` for all permutations `M`. -/
+/-- If `lineInCubicPerm S`, then `lineInCubicPerm (M S)` for all permutations `M`. -/
 lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
     (hS : LineInCubicPerm S) (M' : (FamilyPermutations (2 * n + 1)).group) :
     LineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) := by
diff --git a/HepLean/AnomalyCancellation/PureU1/Sort.lean b/HepLean/AnomalyCancellation/PureU1/Sort.lean
index 92a9a70..e986648 100644
--- a/HepLean/AnomalyCancellation/PureU1/Sort.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Sort.lean
@@ -21,7 +21,7 @@ namespace PureU1
 
 variable {n : ℕ}
 
-/-- We say a charge is shorted if for all `i ≤ j`, then `S i ≤ S j`. -/
+/-- A charge is sorted if for all `i ≤ j`, then `S i ≤ S j`. -/
 @[simp]
 def Sorted {n : ℕ} (S : (PureU1 n).Charges) : Prop :=
    ∀ i j (_ : i ≤ j), S i ≤ S j
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
index 97dd77a..b23fcdb 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -52,7 +52,7 @@ instance : AddCommGroup F.HalfEdgeMomenta := Pi.addCommGroup
 
 instance : Module ℝ F.HalfEdgeMomenta := Pi.module _ _ _
 
-/-- An auxillary function used to define the Euclidean inner product on `F.HalfEdgeMomenta`. -/
+/-- An auxiliary function used to define the Euclidean inner product on `F.HalfEdgeMomenta`. -/
 def euclidInnerAux (x : F.HalfEdgeMomenta) : F.HalfEdgeMomenta →ₗ[ℝ] ℝ where
   toFun y := ∑ i, (x i) * (y i)
   map_add' z y :=
@@ -77,7 +77,7 @@ def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] 
     simp only [euclidInnerAux_symm, LinearMapClass.map_smul, smul_eq_mul, RingHom.id_apply,
       LinearMap.smul_apply]
 
-/-- The type which assocaites to each ege a `1`-dimensional vector space.
+/-- The type which associates to each edge a `1`-dimensional vector space.
  Corresponding to that spanned by its total outflowing momentum. -/
 def EdgeMomenta : Type := F.𝓔 → ℝ
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
index de163c7..417371e 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@@ -23,7 +23,7 @@ open CKMMatrix
 
 noncomputable section
 
-/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard paramaterization of the CKM matrix
+/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard parameterization of the CKM matrix
 as a `3×3` complex matrix. -/
 def standParamAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
   ![![Real.cos θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₃ * exp (-I * δ₁₃)],
@@ -96,8 +96,8 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
     rw [sin_sq, sin_sq]
     ring
 
-/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard paramaterization of the CKM matrix
-as a CKM matrix. -/
+/-- A CKM Matrix from four reals `θ₁₂`, `θ₁₃`, `θ₂₃`,  and `δ₁₃`. This is the standard
+  parameterization of CKM matrices. -/
 def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
   ⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by
    rw [mem_unitaryGroup_iff']
diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index 3112055..ab50ccc 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -151,7 +151,7 @@ lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= by
   refine (inv_eq_left_inv ?h).symm
   exact mem_iff_dual_mul_self.mp Λ.2
 
-/-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/
+/-- The transpose of a matrix in the Lorentz group is an element of the Lorentz group. -/
 def transpose (Λ : LorentzGroup d) : LorentzGroup d :=
   ⟨Λ.1ᵀ, mem_iff_transpose.mp Λ.2⟩
 
diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean
index ff85c66..ce829c0 100644
--- a/HepLean/SpaceTime/LorentzVector/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Basic.lean
@@ -22,7 +22,7 @@ variable (d : ℕ)
 /-- The type of Lorentz Vectors in `d`-space dimensions. -/
 def LorentzVector : Type := (Fin 1 ⊕ Fin d) → ℝ
 
-/-- An instance of a additive commutative monoid on `LorentzVector`. -/
+/-- An instance of an additive commutative monoid on `LorentzVector`. -/
 instance : AddCommMonoid (LorentzVector d) := Pi.addCommMonoid
 
 /-- An instance of a module on `LorentzVector`. -/
diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean
index dbea26e..fa10338 100644
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@@ -23,7 +23,7 @@ open Matrix
 # The definition of the Minkowski Matrix
 
 -/
-/-- The `d.succ`-dimensional real of the form `diag(1, -1, -1, -1, ...)`. -/
+/-- The `d.succ`-dimensional real matrix of the form `diag(1, -1, -1, -1, ...)`. -/
 def minkowskiMatrix {d : ℕ} : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin d) ℝ
 
@@ -146,7 +146,7 @@ lemma self_eq_time_minus_norm : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 :
   rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
   noncomm_ring
 
-/-- The Minkowski metric is symmetric. -/
+/-- The Minkowski metric is symmetric in its arguments.. -/
 lemma symm : ⟪v, w⟫ₘ = ⟪w, v⟫ₘ := by
   simp only [as_sum]
   ac_rfl
diff --git a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
index 2d3257d..9eadda7 100644
--- a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
+++ b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
@@ -130,7 +130,7 @@ lemma rotateMatrix_specialUnitary {φ : HiggsVec} (hφ : φ ≠ 0) :
   mem_specialUnitaryGroup_iff.mpr ⟨rotateMatrix_unitary hφ, rotateMatrix_det hφ⟩
 
 /-- Given a Higgs vector, an element of the gauge group which puts the first component of the
-vector to zero, and the second component to a real -/
+vector to zero, and the second component to a real number. -/
 def rotateGuageGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroup :=
     ⟨1, ⟨(rotateMatrix φ), rotateMatrix_specialUnitary hφ⟩, 1⟩
 
diff --git a/lakefile.toml b/lakefile.toml
index 6dc2426..0fd75e1 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -16,6 +16,13 @@ rev = "v4.10.0-rc1"
 [[lean_lib]]
 name = "HepLean"
 
+# -- Optional inclusion of llm. Needed for `openAI_doc_check`
+# TODO: Move over to `leanprover-community/llm` versions there are bumped.  
+#[[require]]
+#name = "llm"
+#git = "https://github.com/jstoobysmith/Lean_llm_fork"
+#rev = "main"
+
 # -- Optional inclusion of tryAtEachStep
 #[[require]]
 #name = "tryAtEachStep" 
@@ -52,4 +59,9 @@ srcDir = "scripts"
 
 [[lean_exe]]
 name = "stats"
-srcDir = "scripts"
\ No newline at end of file
+srcDir = "scripts"
+
+# -- Optional inclusion of openAI_doc_check. Needs `llm` above.
+#[[lean_exe]]
+#name = "openAI_doc_check"
+#srcDir = "scripts"
\ No newline at end of file
diff --git a/scripts/README.md b/scripts/README.md
index bb0b952..6a49ffb 100644
--- a/scripts/README.md
+++ b/scripts/README.md
@@ -37,6 +37,37 @@ Run using
 lake exe type_former_lint
 ```
 
+## stats.sh 
+
+Outputs statistics for HepLean. 
+
+Run using 
+```
+lake exe stats
+```
+
+## openAI_doc_check.lean 
+
+Uses openAI's API to check for spelling mistakes etc. in doc strings. 
+
+This code needs `https://github.com/jstoobysmith/Lean_llm_fork` to be installed. 
+
+It also needs the enviroment variable `OPENAI_API_KEY` defined using e.g. 
+```
+export OPENAI_API_KEY=<Your-openAI-key>
+```
+
+Run on a specific file using 
+```
+lake exe openAI_doc_check <module_name>
+```
+where `<module_name>` is e.g. `HepLean.SpaceTime.Basic`. 
+
+Run on a random file using 
+```
+lake exe openAI_doc_check random
+```
+
 ## lint-all.sh 
 
 Performs all linting checks on HepLean. 
diff --git a/scripts/hepLean_style_lint.lean b/scripts/hepLean_style_lint.lean
index 9fa8e51..c1c709f 100644
--- a/scripts/hepLean_style_lint.lean
+++ b/scripts/hepLean_style_lint.lean
@@ -83,7 +83,8 @@ def hepLeanLintFile (path : FilePath) : IO Bool := do
   let allOutput := (Array.map (fun lint ↦
     (Array.map (fun (e, n, c) ↦ HepLeanErrorContext.mk e n c path)) (lint lines)))
     #[doubleEmptyLineLinter, doubleSpaceLinter, substringLinter ".-/", substringLinter " )",
-    substringLinter "( ", substringLinter "=by", substringLinter "  def "]
+    substringLinter "( ", substringLinter "=by", substringLinter "  def ",
+    substringLinter "/-- We "]
   let errors := allOutput.flatten
   printErrors errors
   return errors.size > 0
diff --git a/scripts/openAI_doc_check.lean b/scripts/openAI_doc_check.lean
new file mode 100644
index 0000000..3fe0740
--- /dev/null
+++ b/scripts/openAI_doc_check.lean
@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Batteries.Lean.IO.Process
+import Lean
+import Lean.Parser
+import Lean.Data.Json
+import Mathlib.Lean.CoreM
+import LLM.GPT.Json
+import LLM.GPT.API
+/-!
+
+# HepLean OpenAI doc check
+
+This file uses the openAI API to check the doc strings of definitions and theorems in a
+Lean 4 file.
+
+It currently depends on `https://github.com/jstoobysmith/Lean_llm_fork` being imported,
+which is currently not by default.
+
+-/
+open Lean
+open LLM
+open System Meta
+
+def getDocString (constName : Array ConstantInfo) : MetaM String := do
+  let env ← getEnv
+  let mut docString := ""
+  for c in constName do
+    if ¬ Lean.Name.isInternalDetail c.name then
+        let doc ← Lean.findDocString? env c.name
+        match doc with
+        | some x => docString := docString ++ "- " ++ x ++ "\n"
+        | none =>  docString := docString
+  return docString
+
+def header : String := "
+  Answer as if you an expert mathematician, physicist and software engineer.
+  Below I have listed the doc strings of definitions and theorems in a Lean 4 file.
+  Output a list of 1) spelling mistakes. 2) grammatical errors. 3) suggestions for improvement.
+  Note that text within `...` should be treated as code and not spellchecked. Doc strings
+  should be a complete sentence, or a noun phrase.
+
+
+"
+
+def main (args : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  let firstArg := args.head?
+  match firstArg with
+  | some x => do
+    let mut imp : Import := Import.mk x.toName false
+    if x == "random" then
+      let mods : Name :=  `HepLean
+      let imps :  Import := {module := mods}
+      let mFile ← findOLean imps.module
+      unless (← mFile.pathExists) do
+            throw <| IO.userError s!"object file '{mFile}' of module {imps.module} does not exist"
+      let (hepLeanMod, _) ← readModuleData mFile
+      let imports := hepLeanMod.imports
+      let y ← IO.rand 0 (imports.size -1)
+      imp := imports.get! y
+    let mFile ← findOLean imp.module
+    let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean"
+    IO.println s!"Checking: {filePath}"
+    let (modData, _) ← readModuleData mFile
+    let cons := modData.constants
+    let docString ← CoreM.withImportModules #[imp.module] (getDocString cons).run'
+    let message : LLM.Message := {role := Role.user, content := header ++ docString}
+    let request : GPT.Request := {messages := [message]}
+    let response ← LLM.GPT.chat (toString <| ToJson.toJson request)
+    let parsedRespone := GPT.parse response
+    match parsedRespone with
+    | .ok x => IO.println x
+    | .error e => IO.println e
+  | none => IO.println "No module provided."
+  return 0
diff --git a/scripts/stats.lean b/scripts/stats.lean
index cdfa2b8..3a14bca 100644
--- a/scripts/stats.lean
+++ b/scripts/stats.lean
@@ -16,6 +16,7 @@ This file concerns with statistics of HepLean.
 
 -/
 
+
 open Lean System Meta
 
 structure FileStats where