diff --git a/FormalConjectures/OEIS/63880.lean b/FormalConjectures/OEIS/63880.lean
new file mode 100644
index 000000000..b362f2b81
--- /dev/null
+++ b/FormalConjectures/OEIS/63880.lean
@@ -0,0 +1,112 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+import FormalConjectures.Util.ProblemImports
+import FormalConjecturesForMathlib
+
+open scoped ArithmeticFunction
+
+/-!
+# Conjectures associated with A063880
+
+A063880 lists numbers $n$ such that $\sigma(n) = 2 \cdot \text{usigma}(n)$, where $\sigma(n)$ is the
+sum of all divisors and $\text{usigma}(n)$ is the sum of unitary divisors.
+
+Equivalently, these are numbers whose unitary and non-unitary divisors have equal sum.
+
+The conjectures state that all members satisfy $n \equiv 108 \pmod{216}$, and that all
+primitive terms (those whose proper divisors aren't in the sequence) are powerful numbers,
+with $108$ being the only primitive term.
+
+*References:* [oeis.org/A063880](https://oeis.org/A063880)
+-/
+
+namespace OeisA63880
+
+/-- The set of unitary divisors of $n$: divisors $d$ such that $\gcd(d, n/d) = 1$. -/
+def unitaryDivisors (n : ℕ) : Finset ℕ :=
+  {d ∈ n.divisors | d.Coprime (n / d)}
+
+/-- The sum of unitary divisors of $n$, denoted $\text{usigma}(n)$. -/
+def usigma (n : ℕ) : ℕ :=
+  ∑ d ∈ unitaryDivisors n, d
+
+/-- A number $n$ is in the sequence A063880 if $\sigma(n) = 2 \cdot \text{usigma}(n)$. -/
+def a (n : ℕ) : Prop :=
+  0 < n ∧ σ 1 n = 2 * usigma n
+
+/-- The set of numbers in the sequence A063880. -/
+def A : Set ℕ := {n | a n}
+
+/-- A term $n$ is primitive if no proper divisor of $n$ is in the sequence. -/
+abbrev isPrimitiveTerm (n : ℕ) : Prop := A.IsPrimitive n
+
+/-- $108$ is in the sequence A063880. -/
+@[category test, AMS 11]
+theorem a_108 : a 108 := by
+  refine ⟨by norm_num, ?_⟩
+  decide
+
+/-- $540$ is in the sequence A063880. -/
+@[category test, AMS 11]
+theorem a_540 : a 540 := by
+  refine ⟨by norm_num, ?_⟩
+  decide
+
+/-- $756$ is in the sequence A063880. -/
+@[category test, AMS 11]
+theorem a_756 : a 756 := by
+  refine ⟨by norm_num, ?_⟩
+  decide
+
+/-- $108$ is a primitive term. -/
+@[category test, AMS 11]
+theorem isPrimitiveTerm_108 : isPrimitiveTerm 108 := by
+  rw [isPrimitiveTerm, Set.isPrimitive_iff]
+  refine ⟨a_108, ?_⟩
+  intro d hd
+  have ⟨hdvd, hlt⟩ := Nat.mem_properDivisors.mp hd
+  interval_cases d <;> simp_all [A, a] <;> decide
+
+/-- All members of the sequence satisfy $n \equiv 108 \pmod{216}$. -/
+@[category research open, AMS 11]
+theorem mod_216_of_a {n : ℕ} (h : a n) : n % 216 = 108 := by
+  sorry
+
+/-- All primitive terms are powerful numbers. -/
+@[category undergraduate, AMS 11]
+theorem powerful_of_isPrimitiveTerm {n : ℕ} (h : isPrimitiveTerm n) : n.Powerful := by
+  sorry
+
+/-- $108$ is the only primitive term. -/
+@[category research open, AMS 11]
+theorem unique_primitive_108 {n : ℕ} (h : isPrimitiveTerm n) : n = 108 := by
+  sorry
+
+/-- If $m$ is a primitive term and $s$ is squarefree with $\gcd(m, s) = 1$, then $m \cdot s$
+is in the sequence. -/
+@[category undergraduate, AMS 11]
+theorem a_of_primitive_mul_squarefree (m s : ℕ) (hm : isPrimitiveTerm m)
+    (hs : Squarefree s) (hcoprime : m.Coprime s) : a (m * s) := by
+  sorry
+
+/-- Non-primitive terms have the form $m \cdot s$ where $m$ is primitive and $s$ is
+squarefree with $\gcd(m, s) = 1$. -/
+@[category research solved, AMS 11]
+theorem exists_primitive_of_a {n : ℕ} (h : a n) :
+    ∃ m s, isPrimitiveTerm m ∧ Squarefree s ∧ m.Coprime s ∧ n = m * s := by
+  sorry
+
+end OeisA63880
diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
index 68f92a135..1fc0b6af9 100644
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -73,6 +73,7 @@ import FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic
 import FormalConjecturesForMathlib.NumberTheory.Lacunary
 import FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic
 import FormalConjecturesForMathlib.NumberTheory.PrimeGap
+import FormalConjecturesForMathlib.NumberTheory.Primitive
 import FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes
 import FormalConjecturesForMathlib.Order.Filter.Cofinite
 import FormalConjecturesForMathlib.Order.Filter.atTopBot.Finset
diff --git a/FormalConjecturesForMathlib/NumberTheory/Primitive.lean b/FormalConjecturesForMathlib/NumberTheory/Primitive.lean
new file mode 100644
index 000000000..6d45f4c66
--- /dev/null
+++ b/FormalConjecturesForMathlib/NumberTheory/Primitive.lean
@@ -0,0 +1,90 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import Mathlib.Data.Nat.Squarefree
+
+/-!
+# Primitive elements of a set with respect to divisibility
+
+An element `n` is *primitive* in a set `S ⊆ ℕ` if `n ∈ S` and no proper divisor of `n` is in `S`.
+
+This concept appears naturally when studying sequences closed under "divisor inheritance" -
+if every member `n` of a sequence has the property that `m * n` is also in the sequence
+for coprime `m`, then the primitive elements generate the entire sequence.
+
+## Main definitions
+
+* `Set.IsPrimitive`: A natural number `n` is primitive in `S` if `n ∈ S` and
+  `n.properDivisors` is disjoint from `S`.
+* `Set.primitives`: The set of primitive elements of `S`.
+
+## Main results
+
+* `Set.IsPrimitive.mem`: A primitive element is in the set.
+* `Set.IsPrimitive.not_mem_of_properDivisor`: Proper divisors of a primitive element are not
+  in the set.
+* `Set.one_isPrimitive_iff`: `1` is primitive in `S` iff `1 ∈ S`.
+* `Set.prime_isPrimitive_iff`: A prime `p` is primitive in `S` iff `p ∈ S` and `1 ∉ S`.
+-/
+
+namespace Set
+
+/-- An element `n` is *primitive* in a set `S ⊆ ℕ` if `n ∈ S` and no proper divisor of `n`
+is in `S`. -/
+def IsPrimitive (S : Set ℕ) (n : ℕ) : Prop :=
+  n ∈ S ∧ Disjoint (n.properDivisors : Set ℕ) S
+
+/-- The set of primitive elements of `S`. -/
+def primitives (S : Set ℕ) : Set ℕ :=
+  {n | S.IsPrimitive n}
+
+theorem IsPrimitive.mem {S : Set ℕ} {n : ℕ} (h : S.IsPrimitive n) : n ∈ S := h.1
+
+theorem IsPrimitive.disjoint_properDivisors {S : Set ℕ} {n : ℕ} (h : S.IsPrimitive n) :
+    Disjoint (n.properDivisors : Set ℕ) S := h.2
+
+theorem IsPrimitive.not_mem_of_properDivisor {S : Set ℕ} {n d : ℕ} (h : S.IsPrimitive n)
+    (hd : d ∈ n.properDivisors) : d ∉ S :=
+  Set.disjoint_left.mp h.2 hd
+
+theorem IsPrimitive.not_mem_of_dvd_of_lt {S : Set ℕ} {n d : ℕ} (h : S.IsPrimitive n)
+    (hdvd : d ∣ n) (hlt : d < n) : d ∉ S :=
+  h.not_mem_of_properDivisor (Nat.mem_properDivisors.mpr ⟨hdvd, hlt⟩)
+
+theorem isPrimitive_iff {S : Set ℕ} {n : ℕ} :
+    S.IsPrimitive n ↔ n ∈ S ∧ ∀ d ∈ n.properDivisors, d ∉ S := by
+  simp only [IsPrimitive, Set.disjoint_left, Finset.mem_coe]
+
+theorem isPrimitive_iff' {S : Set ℕ} {n : ℕ} (_hn : 0 < n) :
+    S.IsPrimitive n ↔ n ∈ S ∧ ∀ d, d ∣ n → d < n → d ∉ S := by
+  rw [isPrimitive_iff]
+  constructor <;> intro ⟨hmem, hdiv⟩
+  · exact ⟨hmem, fun d hd hlt => hdiv d (Nat.mem_properDivisors.mpr ⟨hd, hlt⟩)⟩
+  · exact ⟨hmem, fun d hd => hdiv d (Nat.mem_properDivisors.mp hd).1 (Nat.mem_properDivisors.mp hd).2⟩
+
+theorem mem_primitives_iff {S : Set ℕ} {n : ℕ} : n ∈ S.primitives ↔ S.IsPrimitive n := Iff.rfl
+
+@[simp]
+theorem primitives_subset {S : Set ℕ} : S.primitives ⊆ S := fun _ h => h.mem
+
+theorem one_isPrimitive_iff {S : Set ℕ} : S.IsPrimitive 1 ↔ 1 ∈ S := by
+  simp [isPrimitive_iff, Nat.properDivisors_one]
+
+theorem prime_isPrimitive_iff {S : Set ℕ} {p : ℕ} (hp : p.Prime) :
+    S.IsPrimitive p ↔ p ∈ S ∧ 1 ∉ S := by
+  simp [isPrimitive_iff, hp.properDivisors]
+
+end Set