diff --git a/FormalConjectures/ErdosProblems/423.lean b/FormalConjectures/ErdosProblems/423.lean
new file mode 100644
index 0000000000..d57fe0ab38
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/423.lean
@@ -0,0 +1,99 @@
+/-
+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
+
+/-!
+# Erdős Problem 423
+
+*Reference:* [erdosproblems.com/423](https://www.erdosproblems.com/423)
+
+Let $a_1 = 1$ and $a_2 = 2$, and for $k \ge 3$ choose $a_k$ to be the least integer
+$> a_{k-1}$ which is the sum of at least two consecutive terms of the sequence. What is
+the asymptotic behaviour of this sequence?
+
+The sequence begins $1, 2, 3, 5, 6, 8, 10, 11, \ldots$ (OEIS A005243).
+
+Asked by Hofstadter (Erdős says Hofstadter was inspired by a similar question of Ulam).
+Bolan and Tang have independently proved that $a_n - n$ is nondecreasing and unbounded,
+so there are infinitely many integers not appearing in the sequence.
+
+[Er77c] Erdős, P., *Problems and results on combinatorial number theory. III*,
+Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976), 1977, pp. 43–72.
+
+[ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial
+number theory*, Monographies de L'Enseignement Mathématique (1980).
+
+[Bolan] Bolan, M., *Hofstader–Ulam Sequence*,
+https://github.com/mjtb49/HofstaderUlam/blob/main/HofstaderUlamSequence.pdf
+
+[Tang] Tang, Q., *On Erdős Problem 423*,
+https://github.com/QuanyuTang/erdos-problem-423/blob/main/On_Erd%C5%91s_Problem_423.pdf
+-/
+
+open Finset BigOperators
+
+namespace Erdos423
+
+/-- `IsConsecutiveBlockSum a k m` means that $m$ equals the sum of at least two
+    consecutive terms of the sequence $a$, using indices from $\{1, \ldots, k - 1\}$.
+    That is, there exist $i, j$ with $1 \le i$, $i + 1 \le j$, $j \le k - 1$ such that
+    $m = a(i) + a(i+1) + \cdots + a(j)$. -/
+def IsConsecutiveBlockSum (a : ℕ → ℕ) (k : ℕ) (m : ℕ) : Prop :=
+  ∃ i j : ℕ, 1 ≤ i ∧ i + 1 ≤ j ∧ j + 1 ≤ k ∧
+    m = ∑ l ∈ Finset.Icc i j, a l
+
+/-- The Hofstadter sequence (OEIS A005243): $a(1) = 1$, $a(2) = 2$, and for $k \ge 3$,
+    $a(k)$ is the least integer $> a(k-1)$ that equals the sum of at least two
+    consecutive terms from $\{a(1), \ldots, a(k-1)\}$. -/
+def IsHofstadterSeq (a : ℕ → ℕ) : Prop :=
+  a 1 = 1 ∧ a 2 = 2 ∧
+  ∀ k : ℕ, 3 ≤ k →
+    IsConsecutiveBlockSum a k (a k) ∧
+    a (k - 1) < a k ∧
+    ∀ m : ℕ, a (k - 1) < m → m < a k → ¬IsConsecutiveBlockSum a k m
+
+/--
+Erdős Problem 423 [Er77c, p.71; ErGr80, p.83]:
+
+Let $a(1) = 1$, $a(2) = 2$, and for $k \ge 3$ let $a(k)$ be the least integer greater
+than $a(k-1)$ that is a sum of at least two consecutive terms of the sequence.
+Then $a(n) - n \to \infty$ as $n \to \infty$.
+
+Equivalently, there are infinitely many positive integers not in the range of $a$.
+This was proved independently by Bolan and Tang. The full asymptotic behaviour
+of the sequence remains an open question.
+-/
+@[category research solved, AMS 5 11]
+theorem erdos_423 :
+    ∀ a : ℕ → ℕ, IsHofstadterSeq a →
+    ∀ M : ℕ, ∃ N : ℕ, ∀ n : ℕ, N ≤ n → M + n ≤ a n := by
+  sorry
+
+/--
+Erdős Problem 423 — nondecreasing variant [Bolan; Tang]:
+
+The sequence $a(n) - n$ is nondecreasing. This is a stronger structural property than
+the unboundedness stated in `erdos_423`, and was also proved independently by Bolan and
+Tang.
+-/
+@[category research solved, AMS 5 11]
+theorem erdos_423_nondecreasing :
+    ∀ a : ℕ → ℕ, IsHofstadterSeq a →
+    ∀ n m : ℕ, n ≤ m → a n - n ≤ a m - m := by
+  sorry
+
+end Erdos423
diff --git a/FormalConjectures/ErdosProblems/839.lean b/FormalConjectures/ErdosProblems/839.lean
new file mode 100644
index 0000000000..6470ed9417
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/839.lean
@@ -0,0 +1,77 @@
+/-
+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.Data.Set.Density
+
+/-!
+# Erdős Problem 839
+
+*Reference:* [erdosproblems.com/839](https://www.erdosproblems.com/839)
+
+Given a strictly increasing sequence of positive integers where no term equals the sum of
+consecutive earlier terms, is it true that $\limsup a_n / n = \infty$? A stronger form asks
+whether $(1/\log x) \sum_{a_n < x} 1/a_n \to 0$.
+
+A problem of Erdős [Er78f][Er92c].
+
+[Er78f] Erdős, P., *Problems in number theory and combinatorics*, Proc. Sixth Manitoba Conf. on
+Numerical Math. (1978), 35-58.
+
+[Er92c] Erdős, P., *Some of my favourite unsolved problems*, J. Combin. Theory Ser. A (1992).
+
+[Fr93] Freud, R., *Adding numbers — on a problem of P. Erdős*, James Cook Mathematical Notes
+(1993), 6199–6202.
+-/
+
+open Filter Real Finset
+
+namespace Erdos839
+
+/-- A sequence $a : \mathbb{N} \to \mathbb{N}$ is "sum-of-consecutive-free" if no term equals
+the sum of a contiguous block of earlier terms. That is, for all $i$,
+$a_i \neq a_j + a_{j+1} + \cdots + a_k$ for any $j \leq k < i$. -/
+def SumOfConsecutiveFree (a : ℕ → ℕ) : Prop :=
+  ∀ i : ℕ, ∀ j k : ℕ, j ≤ k → k < i →
+    a i ≠ ∑ l ∈ Finset.Icc j k, a l
+
+/--
+Erdős Problem 839 (Part 1) [Er78f][Er92c]:
+
+Let $1 \leq a_1 < a_2 < \cdots$ be a strictly increasing sequence of positive integers
+such that no $a_i$ is the sum of consecutive $a_j$ for $j < i$.
+Is it true that $\limsup a_n / n = \infty$?
+-/
+@[category research open, AMS 11]
+theorem erdos_839 : answer(sorry) ↔
+    ∀ (a : ℕ → ℕ), (∀ n, 1 ≤ a n) → StrictMono a → SumOfConsecutiveFree a →
+    ∀ M : ℝ, ∃ᶠ n in atTop, M < (a n : ℝ) / (n : ℝ) := by
+  sorry
+
+/--
+Erdős Problem 839 (Part 2, stronger) [Er78f][Er92c]:
+
+Let $1 \leq a_1 < a_2 < \cdots$ be a strictly increasing sequence of positive integers
+such that no $a_i$ is the sum of consecutive $a_j$ for $j < i$.
+Is it true that $\lim_{x \to \infty} \frac{1}{\log x} \sum_{a_n < x} \frac{1}{a_n} = 0$?
+-/
+@[category research open, AMS 11]
+theorem erdos_839.variants.stronger : answer(sorry) ↔
+    ∀ (a : ℕ → ℕ), (∀ n, 1 ≤ a n) → StrictMono a → SumOfConsecutiveFree a →
+    Set.HasLogDensity (Set.range a) 0 := by
+  sorry
+
+end Erdos839