chore: Add missing spaces in docstrings (google-deepmind#1840)

felixpernegger · web-flow · commit 5f51218e16c6 · 2026-01-22T08:12:40.000+01:00
diff --git a/FormalConjectures/Arxiv/1308.0994/BoxdotConjecture.lean b/FormalConjectures/Arxiv/1308.0994/BoxdotConjecture.lean
@@ -160,7 +160,7 @@ structure NormalModalLogic : Type where
   /-- `extK` means that if `K ⊢ φ`, then `φ ∈ thms`. That is, the logic extends system K. -/
   extK : ∀ {φ}, KProof ∅ φ → φ ∈ thms
   /-- `mp` means that if `φ ∈ thms` and `(φ ~> ψ) ∈ thms`, then `ψ ∈ thms`. That is, thms is closed
-  under modus ponens.-/
+  under modus ponens. -/
   mp : ∀ {φ ψ}, φ ∈ thms → (φ ~> ψ) ∈ thms → ψ ∈ thms
   /-- `nec` means that if `φ ∈ thms`, then `□φ ∈ thms`. Equivalently, `thms` is closed under
   necessitation -/
diff --git a/FormalConjectures/ErdosProblems/1054.lean b/FormalConjectures/ErdosProblems/1054.lean
@@ -27,7 +27,7 @@ namespace Erdos1054
 open Classical Filter Asymptotics
 
 /-- Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest
-divisors of $m$ for some $k\geq 1$.-/
+divisors of $m$ for some $k\geq 1$. -/
 noncomputable def f (n : ℕ) : ℕ :=
   if h : ∃ᵉ (m) (k ≥ 1), n = ∑ i < k, Nat.nth (· ∈ m.divisors) i then
     Nat.find h
diff --git a/FormalConjectures/ErdosProblems/1055.lean b/FormalConjectures/ErdosProblems/1055.lean
@@ -26,7 +26,7 @@ namespace Erdos1055
 
 /-- A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are
 $2$ or $3$. In general, a prime $p$ is in class $r$ if every prime factor
-of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor.-/
+of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor. -/
 def IsOfClass : ℕ+ → ℕ → Prop := fun r ↦
   PNat.caseStrongInductionOn (p := fun (_ : ℕ+) ↦ ℕ → Prop) r
     (fun p ↦ (p + 1).primeFactors ⊆ {2, 3})
@@ -49,7 +49,7 @@ open Classical
 /-- A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are
 $2$ or $3$. In general, a prime $p$ is in class $r$ if every prime factor
 of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor.
-Let $p_r$ is the least prime in class $r$.-/
+Let $p_r$ is the least prime in class $r$. -/
 noncomputable def p (r : ℕ+) : ℕ := Nat.find (exists_p r)
 
 /-- A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are
diff --git a/FormalConjectures/ErdosProblems/1072.lean b/FormalConjectures/ErdosProblems/1072.lean
@@ -27,7 +27,7 @@ open scoped Topology
 
 namespace Erdos1072
 
-/-- For any prime $p$, let $f(p)$ be the least integer such that $f(p)! + 1 \equiv 0 \mod p$.-/
+/-- For any prime $p$, let $f(p)$ be the least integer such that $f(p)! + 1 \equiv 0 \mod p$. -/
 noncomputable def f (p : ℕ) : ℕ := sInf {n | (n)! + 1 ≡ 0 [MOD p]}
 
 /-- Is it true that there are infinitely many $p$ for which $f(p) = p − 1$? -/
diff --git a/FormalConjectures/ErdosProblems/1074.lean b/FormalConjectures/ErdosProblems/1074.lean
@@ -25,7 +25,7 @@ import FormalConjectures.Util.ProblemImports
 open scoped Nat
 
 /-- The EHS numbers (after Erdős, Hardy, and Subbarao) are those $m\geq 1$ such that there
-exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$.-/
+exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$. -/
 abbrev Nat.EHSNumbers : Set ℕ := {m | 1 ≤ m ∧ ∃ p, p.Prime ∧ ¬p ≡ 1 [MOD m] ∧ p ∣ m ! + 1}
 
 /-- The Pillai primes are those primes $p$ such that there exists an $m$ with
@@ -76,7 +76,7 @@ theorem erdos_1074.parts_ii_ii :
   sorry
 
 /-- Pillai [Pi30] raised the question of whether there exist any primes in $P$. This was answered
-by Chowla, who noted that, for example, $14! + 1 \equiv 18! + 1 \equiv 0 \pmod{23}$.-/
+by Chowla, who noted that, for example, $14! + 1 \equiv 18! + 1 \equiv 0 \pmod{23}$. -/
 @[category test, AMS 11]
 theorem erdos_1074.variants.mem_pillaiPrimes : 23 ∈ PillaiPrimes := by
   norm_num
diff --git a/FormalConjectures/ErdosProblems/168.lean b/FormalConjectures/ErdosProblems/168.lean
@@ -26,17 +26,17 @@ open scoped Topology
 
 namespace Erdos168
 
-/--Say a finite set of natural numbers is *non ternary* if it contains no
-3-term arithmetic progression of the form `n, 2n, 3n`.-/
+/-- Say a finite set of natural numbers is *non ternary* if it contains no
+3-term arithmetic progression of the form `n, 2n, 3n`. -/
 def NonTernary (S : Finset ℕ) : Prop := ∀ n : ℕ, n ∉ S ∨ 2*n ∉ S ∨ 3*n ∉ S
 
 /--`IntervalNonTernarySets N` is the (fin)set of non ternary subsets of `{1,...,N}`.
-The advantage of defining it as below is that some proofs (e.g. that of `F 3 = 2`) become `rfl`.-/
+The advantage of defining it as below is that some proofs (e.g. that of `F 3 = 2`) become `rfl`. -/
 def IntervalNonTernarySets (N : ℕ) : Finset (Finset ℕ) :=
   (Finset.Icc 1 N).powerset.filter
     fun S => ∀ n ∈ Finset.Icc 1 (N / 3 : ℕ), n ∉ S ∨ 2*n ∉ S ∨ 3*n ∉ S
 
-/--`F N` is the size of the largest non ternary subset of `{1,...,N}`.-/
+/--`F N` is the size of the largest non ternary subset of `{1,...,N}`. -/
 abbrev F (N : ℕ) : ℕ := (IntervalNonTernarySets N).sup Finset.card
 
 @[category API, AMS 5 11]
diff --git a/FormalConjectures/ErdosProblems/229.lean b/FormalConjectures/ErdosProblems/229.lean
@@ -35,7 +35,7 @@ $$
 Solved in the affirmative by Barth and Schneider [BaSc72].
 
 [BaSc72] Barth, K. F. and Schneider, W. J., _On a problem of Erdős concerning the zeros of_
-_the derivatives of an entire function_. Proc. Amer. Math. Soc. (1972), 229--232.-/
+_the derivatives of an entire function_. Proc. Amer. Math. Soc. (1972), 229--232. -/
 @[category research solved, AMS 30]
 theorem erdos_229 :
     letI := Polynomial.algebraPi ℂ ℂ ℂ
diff --git a/FormalConjectures/ErdosProblems/244.lean b/FormalConjectures/ErdosProblems/244.lean
@@ -34,7 +34,7 @@ theorem erdos_244 : answer(sorry) ↔
 /-- Romanoff [Ro34] proved that the answer is yes if $C$ is an integer.
 
 [Ro34] Romanoff, N. P., _Über einige Sätze der additiven Zahlentheorie_.
-Math. Ann. (1934), 668-678.-/
+Math. Ann. (1934), 668-678. -/
 @[category research solved, AMS 11]
 theorem erdos_244.variants.Romanoff {C : ℕ} (hC : 1 < C) :
     0 < { p + ⌊C ^ k⌋₊ | (p) (k) (_ : p.Prime) }.lowerDensity := by
diff --git a/FormalConjectures/ErdosProblems/253.lean b/FormalConjectures/ErdosProblems/253.lean
@@ -27,7 +27,7 @@ namespace Erdos253
 open scoped Topology
 
 /-- The predicate that `a : ℕ → ℕ` is a strictly monotone sequence such that every infinite
-arithmetic progression contains infinitely many integers that are the sum of distinct $a_i$s.-/
+arithmetic progression contains infinitely many integers that are the sum of distinct $a_i$s. -/
 @[inline]
 def RepresentsAPs (a : ℕ → ℕ) : Prop :=
     StrictMono a ∧ ∀ l, l.IsAPOfLength ⊤ → (subsetSums (Set.range a) ∩ l).Infinite
diff --git a/FormalConjectures/ErdosProblems/319.lean b/FormalConjectures/ErdosProblems/319.lean
@@ -37,7 +37,7 @@ and
 $$
   \sum_{n\in A'}\frac{\delta n}{n} \neq 0
 $$
-for all non-empty $A'\subsetneq A$.-/
+for all non-empty $A'\subsetneq A$. -/
 @[category research open, AMS 5]
 theorem erdos_319 (N : ℕ) : IsGreatest
     { #A | (A) (_ : A ⊆ Finset.Icc 1 N)
diff --git a/FormalConjectures/ErdosProblems/350.lean b/FormalConjectures/ErdosProblems/350.lean
@@ -24,11 +24,11 @@ import FormalConjectures.Util.ProblemImports
 
 namespace Erdos350
 
-/--The predicate that all (finite) subsets of `A` have distinct sums-/
+/-- The predicate that all (finite) subsets of `A` have distinct sums. -/
 def DistinctSubsetSums {M : Type*} [AddCommMonoid M] (A : Set M) : Prop :=
   Set.Pairwise {X : Finset M | ↑X ⊆ A} fun X Y => X.sum id ≠ Y.sum id
 
-/--The predicate that all (finite) subsets of `A` have distinct sums, decidable version-/
+/-- The predicate that all (finite) subsets of `A` have distinct sums, decidable version -/
 def DecidableDistinctSubsetSums {M : Type*} [AddCommMonoid M] [DecidableEq M] (A : Finset M) : Prop :=
   ∀ X ⊆ A, ∀ Y ⊆ A, X ≠ Y → X.sum id ≠ Y.sum id
 
@@ -44,7 +44,7 @@ theorem distinctSubsetSums_1_2 : DistinctSubsetSums ({1, 2} : Finset ℕ).toSet
   fin_cases hx <;> fin_cases hy <;> simp_all
 
 
-/--Small sanity check: the two predicates are saying the same thing.-/
+/-- Small sanity check: the two predicates are saying the same thing. -/
 @[category API, AMS 5 11]
 theorem DistinctSubsetSums_iff_DecidableDistinctSubsetSums
     {M : Type*} [AddCommMonoid M] [DecidableEq M] (A : Finset M) :
diff --git a/FormalConjectures/ErdosProblems/375.lean b/FormalConjectures/ErdosProblems/375.lean
@@ -52,7 +52,7 @@ theorem erdos_375.bounded_gap : Erdos375 →
     < (n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c) := by
   sorry
 
-/-- In particular, if `Erdos375` is true, then Legendre's conjecture is asymptotically true.-/
+/-- In particular, if `Erdos375` is true, then Legendre's conjecture is asymptotically true. -/
 @[category research solved, AMS 11]
 theorem erdos_375.legendre : Erdos375 →
     (∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p) :=
diff --git a/FormalConjectures/ErdosProblems/402.lean b/FormalConjectures/ErdosProblems/402.lean
@@ -64,7 +64,7 @@ There exists an effectively computable $n_0$ with the following properties:
 $\max_{i, j} \frac{a_i}{(a_i, a_j)} \ge n$.
 (ii) If equality holds then the system $\{a_1, a_2, \dots, a_n\}$ is either of the
 type $\{k, 2k, \dots, nk\}$ or of the type
-$\left\{\frac{k}{1}, \frac{k}{2}, \dots, \frac{k}{n}\right\}$.-/
+$\left\{\frac{k}{1}, \frac{k}{2}, \dots, \frac{k}{n}\right\}$. -/
 @[category research solved, AMS 11]
 theorem erdos_402.variants.szegedy_zaharescu_weak : ∀ᶠ n in atTop,
     ∀ (A : Finset ℕ), A.card = n → 0 ∉ A →
diff --git a/FormalConjectures/ErdosProblems/416.lean b/FormalConjectures/ErdosProblems/416.lean
@@ -27,7 +27,7 @@ open scoped Topology Real
 
 namespace Erdos416
 
-/--Let `V(x)` count the number of `n≤x` such that `ϕ(m)=n` is solvable-/
+/-- Let `V(x)` count the number of `n≤x` such that `ϕ(m)=n` is solvable. -/
 noncomputable abbrev V (x : ℝ) : ℝ :=
   (Finset.Icc 1 ⌊x⌋₊ |>.filter (fun n => ∃ (m : ℕ), m.totient = n)).card
 
diff --git a/FormalConjectures/ErdosProblems/509.lean b/FormalConjectures/ErdosProblems/509.lean
@@ -33,8 +33,8 @@ universe u v
 
 variable {M : Type u} [MetricSpace M]
 
-/--An $r$-bounded disc cover of a subset of a metric space $M$
-is an indexed family of closed discs whose radii sum to at most $r$.-/
+/-- An $r$-bounded disc cover of a subset of a metric space $M$
+is an indexed family of closed discs whose radii sum to at most $r$. -/
 structure BoundedDiscCover (S : Set M) (r : ℝ) (ι : Type v) where
   (C : ι → M)
   (R : ι → ℝ)
diff --git a/FormalConjectures/ErdosProblems/846.lean b/FormalConjectures/ErdosProblems/846.lean
@@ -28,14 +28,14 @@ namespace Erdos846
 section Prelims
 open Classical
 
-/--We say a subset `A` of points in the plane is `ε`-non-trilinear if any subset
-`B` of `A`, contains a non-trilinear subset `C` of size at least `ε|B|`.-/
+/-- We say a subset `A` of points in the plane is `ε`-non-trilinear if any subset
+`B` of `A`, contains a non-trilinear subset `C` of size at least `ε|B|`. -/
 def NonTrilinearFor (A : Set ℝ²) (ε : ℝ) : Prop :=
   ∀ (B : Finset ℝ²), B.toSet ⊆ A → ∃ C ⊆ B,
     ε * B.card ≤ C.card ∧ NonTrilinear C.toSet
 
-/--We say a subset `A` of points in the plane is weakly non-trilinear if it is
-a finite union of non-trilinear sets.-/
+/-- We say a subset `A` of points in the plane is weakly non-trilinear if it is
+a finite union of non-trilinear sets. -/
 def WeaklyNonTrilinear (A : Set ℝ²) : Prop :=
   ∃ B : Finset (Set ℝ²), A = sSup B ∧ ∀ b ∈ B, NonTrilinear b
 
diff --git a/FormalConjectures/ErdosProblems/873.lean b/FormalConjectures/ErdosProblems/873.lean
@@ -24,13 +24,13 @@ import FormalConjectures.Util.ProblemImports
 
 namespace Erdos873
 
-/--Let $a$ be some sequence of natural numbers. We set $F(A,X,k)$ to be the count of
+/-- Let $a$ be some sequence of natural numbers. We set $F(A,X,k)$ to be the count of
 the number of $i$ such that $[a_i,a_{i+1}, \dots ,a_{i+k−1}] < X$,
-where the left-hand side is the least common multiple.-/
+where the left-hand side is the least common multiple. -/
 noncomputable abbrev F (a : ℕ → ℕ) (X : ℝ) (k : ℕ) : ℕ∞ :=
   {i : ℕ | (Finset.range k).lcm (fun m => a (i + m)) < X}.encard
 
-/--Let $A = \{a_1 < a_2 < \dots\} \subseteq \mathbb{N}$ and let $F(A,X,k)$ count the number of $i$
+/-- Let $A = \{a_1 < a_2 < \dots\} \subseteq \mathbb{N}$ and let $F(A,X,k)$ count the number of $i$
 such that $[a_i,a_{i+1}, \dots ,a_{i+k−1}] < X$, where the left-hand side is the least common
 multiple. Is it true that, for every $\epsilon > 0$, there exists some $k$ such that
 $F(A,X,k) < X^\epsilon$?-/
diff --git a/FormalConjectures/ErdosProblems/939.lean b/FormalConjectures/ErdosProblems/939.lean
@@ -79,12 +79,12 @@ theorem erdos_939.variants.examples : (∃ r ≥ 4, (Erdos939Sums r).Nonempty) :
   · norm_num [Nat.Full, Nat.primeFactors, Nat.primeFactorsList]
 
 
-/-- Cambie has also found solutions when $r=7$.-/
+/-- Cambie has also found solutions when $r=7$. -/
 @[category research solved, AMS 11]
 theorem erdos_939.variants.seven : (Erdos939Sums 7).Nonempty := by
   sorry
 
-/-- Cambie has also found solutions when $r=8$.-/
+/-- Cambie has also found solutions when $r=8$. -/
 @[category research solved, AMS 11]
 theorem erdos_939.variants.eight : (Erdos939Sums 8).Nonempty := by
   sorry
diff --git a/FormalConjectures/ErdosProblems/945.lean b/FormalConjectures/ErdosProblems/945.lean
@@ -31,7 +31,7 @@ abbrev τ  := fun (n : ℕ) => n.divisors.card
 
 /--
 Let $F(x)$ be the maximal $k$ such that there exist $n+1, \dots, n+k \le x$
-with $τ(n+1), \dots, τ(n+k)$ all distinct, where $τ(m)$ counts the divisors of $m$.-/
+with $τ(n+1), \dots, τ(n+k)$ all distinct, where $τ(m)$ counts the divisors of $m$. -/
 noncomputable def F (x : ℝ) : ℕ :=
   sSup {k | ∃ (n : ℕ), n + k ≤ x ∧ (Set.Ioc n (n + k)).InjOn τ}
 
diff --git a/FormalConjectures/Mathoverflow/75792.lean b/FormalConjectures/Mathoverflow/75792.lean
@@ -180,7 +180,7 @@ theorem Reachable.five_pow_six : Reachable (5^6) 29 :=
   have h27 : Reachable 27 9 := .pow' 3 3
   .add .one <| .mul h8 <| .mul h9 <| .add .one <| .mul h8 h27
 
-/-- Is `5n` the complexity of `5^n` for `0 < n`? Answer: No.-/
+/-- Is `5n` the complexity of `5^n` for `0 < n`? Answer: No. -/
 @[category research solved, AMS 11]
 theorem complexity_five_pow : answer(False) ↔ ∀ n : ℕ, 0 < n → complexity (5 ^ n) = 5 * n := by
   simp [false_iff, not_forall]
diff --git a/FormalConjectures/Wikipedia/AgohGiuga.lean b/FormalConjectures/Wikipedia/AgohGiuga.lean
@@ -57,17 +57,17 @@ An integer `p ≥ 2` is prime if and only if it satifies the congruence
 def AgohGiugaSum : Prop := ∀ p ≥ 2, p.Prime ↔
   p ∣ 1 + ∑ i ∈ Finset.Ioo 0 p, i^(p - 1 : ℕ)
 
-/--The **Agoh-Giuga Conjecture**, Agoh's formulation-/
+/-- The **Agoh-Giuga Conjecture**, Agoh's formulation -/
 @[category research open, AMS 11]
 theorem agoh_giuga : AgohGiugaCongr := by
   sorry
 
-/--The **Agoh-Giuga Conjecture**, Giuga's formulation-/
+/-- The **Agoh-Giuga Conjecture**, Giuga's formulation -/
 @[category research open, AMS 11]
 theorem agoh_giuga.variants.giuga : AgohGiugaSum := by
   sorry
 
-/--The two statements of the conjecture are equivalent.-/
+/-- The two statements of the conjecture are equivalent. -/
 @[category research solved, AMS 11]
 theorem agoh_giuga.variants.equivalence : AgohGiugaCongr ↔ AgohGiugaSum := by
   sorry
diff --git a/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean b/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean
@@ -51,7 +51,7 @@ open scoped Topology Nat
 
 namespace ArtinPrimitiveRootsConjecture
 
-/--Let $S(a)$ be the set of primes such that $a$ is a primitive root modulo $p$. -/
+/-- Let $S(a)$ be the set of primes such that $a$ is a primitive root modulo $p$. -/
 abbrev S (a : ℤ) : Set ℕ :=
   {p : ℕ | p.Prime ∧ orderOf (a : ZMod p) = (p-1 : ℕ)}
 
diff --git a/FormalConjectures/Wikipedia/FermatCatalanConjecture.lean b/FormalConjectures/Wikipedia/FermatCatalanConjecture.lean
@@ -41,7 +41,7 @@ def FermatCatalanSet' : Set (Fin 6 → ℕ) :=
 def FermatCatalanSet : Set (ℕ × ℕ × ℕ) :=
     (fun f => ((f 0) ^ (f 3), (f 1) ^ (f 4), (f 2) ^ (f 5))) '' FermatCatalanSet'
 
-/--The proposition that the Fermat-Catalan Conjecture is true.-/
+/-- The proposition that the Fermat-Catalan Conjecture is true. -/
 def fermatCatalanConjecture : Prop :=
   FermatCatalanSet.Finite
 
diff --git a/FormalConjectures/Wikipedia/JacobianConjecture.lean b/FormalConjectures/Wikipedia/JacobianConjecture.lean
@@ -33,17 +33,17 @@ variable {σ τ ι : Type*}
 
 variable (k σ τ) in
 
-/--Implicitly use `σ` as an index set and `k` as coefficient ring. -/
+/-- Implicitly use `σ` as an index set and `k` as coefficient ring. -/
 abbrev RegularFunction := τ → MvPolynomial σ k
 
 namespace RegularFunction
 
-/--The Jacobian of a vector valued polynomial function, viewed as a polynomial.-/
+/-- The Jacobian of a vector valued polynomial function, viewed as a polynomial. -/
 noncomputable def Jacobian (F : RegularFunction k σ τ) :
     Matrix σ τ (MvPolynomial σ k) :=
   Matrix.of fun i j => MvPolynomial.pderiv i (F j)
 
-/--The composition of two vector valued polynomial functions.-/
+/-- The composition of two vector valued polynomial functions. -/
 noncomputable def comp
     (F : RegularFunction k σ τ) (G : RegularFunction k τ ι) :
     RegularFunction k σ ι :=
@@ -64,7 +64,7 @@ open RegularFunction
 
 variable {σ : Type*} [Fintype σ]
 
-/--The **Jacobian Conjecture**: any regular function
+/-- The **Jacobian Conjecture**: any regular function
 (i.e. vector valued polynomial function from) `kⁿ → kᵐ`
 whose Jacobian is a non-zero constant has an inverse that
 is given by a regular function, where `k` is a field of characteristic `0`-/
@@ -83,15 +83,15 @@ open RegularFunction
 
 variable {σ τ ι : Type*} [Fintype σ]
 
-/--The evaluation of a regular function `f` over `k` at some point `a`
+/-- The evaluation of a regular function `f` over `k` at some point `a`
 with coordinates in some algebra over `k`-/
 noncomputable def RegularFunction.aeval {S₁ : Type*} [CommSemiring S₁] [Algebra k S₁]
     (F : RegularFunction k σ τ) : (σ → S₁) → τ → S₁ :=
   fun a t ↦ MvPolynomial.aeval a (F t)
 
 
 omit [CharZero k] [Fintype σ] in
-/--`aeval` is compatible with composition of regular functions-/
+/--`aeval` is compatible with composition of regular functions. -/
 @[category API, AMS 14]
 lemma comp_aeval
     (F : RegularFunction k σ τ) (G : RegularFunction k τ ι)
diff --git a/FormalConjectures/Wikipedia/Koethe.lean b/FormalConjectures/Wikipedia/Koethe.lean
@@ -32,45 +32,45 @@ variable [Ring R]
 
 namespace Koethe
 
-/--Say a subset `I` of a ring `R` is nilpotent if all its elements are nilpotent. -/
+/-- Say a subset `I` of a ring `R` is nilpotent if all its elements are nilpotent. -/
 def IsNil {S : Type*} [SetLike S R] (I : S) := ∀ i ∈ I, IsNilpotent i
 
 --TODO(lezeau): add some basic API and already known results for nil ideals
 
 variable (R) in
-/--The *Kothe Radical* of a ring `R` is the sum of all (two-sided) nil ideals of `R`.
+/-- The *Kothe Radical* of a ring `R` is the sum of all (two-sided) nil ideals of `R`.
 Tags: Kothe Radical, upper nilradical-/
 def KotheRadical : TwoSidedIdeal R := sSup {I : TwoSidedIdeal R | IsNil I}
 
 --This is often denoted `Nil*(R)`
 local notation "Nil* " R => KotheRadical R
 
-/--The **Köthe conjecture**: In any ring, the sum of two nil left ideals is nil.-/
+/-- The **Köthe conjecture**: In any ring, the sum of two nil left ideals is nil. -/
 @[category research open, AMS 16]
 theorem KotheConjecture (I J : Ideal R) (hI : IsNil I) (hJ : IsNil J) : IsNil (I + J) := by
   sorry
 
-/--The **Köthe conjecture**: every left nil radical is contained in the Köthe radical.-/
+/-- The **Köthe conjecture**: every left nil radical is contained in the Köthe radical. -/
 @[category research open, AMS 16]
 theorem KotherConjecture.variants.le_KotherRadical {I : Ideal R} (hI : IsNil I) :
     (I : Set R) ⊆ KotheRadical R := by
   sorry
 
-/--The **Köthe conjecture**: for any nil ideal `I` of `R`, the matrix ideal `M_n(I)` is a nil ideal
-of the matrix ring `M_n(R)`.-/
+/-- The **Köthe conjecture**: for any nil ideal `I` of `R`, the matrix ideal `M_n(I)` is a nil ideal
+of the matrix ring `M_n(R)`. -/
 @[category research open, AMS 16]
 theorem KotherConjecture.variants.general_matrix {I : TwoSidedIdeal R} (hI : IsNil I)
     (n : Type*) [Fintype n] : IsNil (matrix n I) := by
   sorry
 
-/--The **Köthe conjecture**: for any nil ideal `I` of `R`, the matrix ideal `M_2(I)` is a nil ideal
-of the matrix ring `M_2(R)`.-/
+/-- The **Köthe conjecture**: for any nil ideal `I` of `R`, the matrix ideal `M_2(I)` is a nil ideal
+of the matrix ring `M_2(R)`. -/
 @[category research open, AMS 16]
 theorem KotherConjecture.variants.two_by_two_matrix {I : TwoSidedIdeal R} (hI : IsNil I) :
     IsNil (matrix (Fin 2) I) := by
   sorry
 
-/--The **Köthe conjecture**: for any positive integer `n`, the Köthe radical of `R` is the matrix ideal `M_2(Nil*(R))`.-/
+/-- The **Köthe conjecture**: for any positive integer `n`, the Köthe radical of `R` is the matrix ideal `M_2(Nil*(R))`. -/
 @[category research open, AMS 16]
 theorem KotherConjecture.variants.matrixOver_KotherRadical
     {I : TwoSidedIdeal R} (hI : IsNil I) (n : Type*) [Fintype n] :
diff --git a/FormalConjectures/Wikipedia/ModularityConjecture.lean b/FormalConjectures/Wikipedia/ModularityConjecture.lean
diff --git a/FormalConjectures/Wikipedia/Sendov.lean b/FormalConjectures/Wikipedia/Sendov.lean
diff --git a/FormalConjecturesForMathlib/Combinatorics/Additive/Basis.lean b/FormalConjecturesForMathlib/Combinatorics/Additive/Basis.lean
diff --git a/FormalConjecturesForMathlib/Computability/TuringMachine/BusyBeavers.lean b/FormalConjecturesForMathlib/Computability/TuringMachine/BusyBeavers.lean
diff --git a/FormalConjecturesForMathlib/Data/Nat/Full.lean b/FormalConjecturesForMathlib/Data/Nat/Full.lean
diff --git a/FormalConjecturesForMathlib/Data/Nat/Squarefree.lean b/FormalConjecturesForMathlib/Data/Nat/Squarefree.lean
diff --git a/FormalConjecturesForMathlib/Geometry/2d.lean b/FormalConjecturesForMathlib/Geometry/2d.lean
