/-
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 FormalConjecturesUtilScholz conjecture on addition chains
References:
Tall22 Amadou Tall. "The Scholz conjecture on addition chain is true for infinitely many integers with $\ell(2n) = \ell(n)$." arXiv:2210.13812 (2022). Also available as ePrint 2023/020.
namespace ScholzConjecturelocal notation "ℓ(" n ")" => additionChainLength nThe Scholz conjecture, also known as the Scholz-Brauer conjecture, asserts that for every positive integer $n$, the addition-chain length of $2^n - 1$ is at most $n - 1 + \ell(n)$.
@[category research open, AMS 11 68]
theorem scholz_conjecture :
answer(sorry) ↔ ∀ (n : ℕ), 0 < n → ℓ(2 ^ n - 1) ≤ n - 1 + ℓ(n) := ⊢ True ↔ ∀ (n : ℕ), 0 < n → ℓ(2 ^ n - 1) ≤ n - 1 + ℓ(n)
All goals completed! 🐙
7 is the first value where the doubling bound is not sharp: it gives ℓ(7) ≥ 3, and no
four-entry chain ends at 7. Every entry of such a chain lies strictly between 1 and 7, so
there are only finitely many to rule out.
@[category API, AMS 11 68]
private lemma three_notMem_additionChainSteps_seven : 3 ∉ additionChainSteps 7 := ⊢ 3 ∉ additionChainSteps 7
c:List ℕhhead:c.head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) chsum:∀ x ∈ c, x ≠ 1 → ∃ y ∈ c, ∃ z ∈ c, x = y + zhlast:c.getLast? = some 7hlen:c.length = 3 + 1⊢ False
match c, hlen with
c:List ℕhlen:c.length = 3 + 1w:ℕx:ℕy:ℕz:ℕx✝:[w, x, y, z].length = 3 + 1hhead:[w, x, y, z].head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) [w, x, y, z]hsum:∀ x_1 ∈ [w, x, y, z], x_1 ≠ 1 → ∃ y_1 ∈ [w, x, y, z], ∃ z_1 ∈ [w, x, y, z], x_1 = y_1 + z_1hlast:[w, x, y, z].getLast? = some 7⊢ False
c:List ℕhlen:c.length = 3 + 1w:ℕx:ℕy:ℕz:ℕx✝:[w, x, y, z].length = 3 + 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) [w, x, y, z]hsum:∀ x_1 ∈ [w, x, y, z], x_1 ≠ 1 → ∃ y_1 ∈ [w, x, y, z], ∃ z_1 ∈ [w, x, y, z], x_1 = y_1 + z_1hlast:[w, x, y, z].getLast? = some 7hhead:w = 1⊢ False
c:List ℕhlen:c.length = 3 + 1w:ℕx:ℕy:ℕz:ℕx✝:[w, x, y, z].length = 3 + 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) [w, x, y, z]hsum:∀ x_1 ∈ [w, x, y, z], x_1 ≠ 1 → ∃ y_1 ∈ [w, x, y, z], ∃ z_1 ∈ [w, x, y, z], x_1 = y_1 + z_1hhead:w = 1hlast:z = 7⊢ False
c:List ℕhlen:c.length = 3 + 1x:ℕy:ℕz:ℕhlast:z = 7x✝:[1, x, y, z].length = 3 + 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) [1, x, y, z]hsum:∀ x_1 ∈ [1, x, y, z], x_1 ≠ 1 → ∃ y_1 ∈ [1, x, y, z], ∃ z_1 ∈ [1, x, y, z], x_1 = y_1 + z_1⊢ False; c:List ℕhlen:c.length = 3 + 1x:ℕy:ℕx✝:[1, x, y, 7].length = 3 + 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) [1, x, y, 7]hsum:∀ x_1 ∈ [1, x, y, 7], x_1 ≠ 1 → ∃ y_1 ∈ [1, x, y, 7], ∃ z ∈ [1, x, y, 7], x_1 = y_1 + z⊢ False
c:List ℕhlen:c.length = 3 + 1x:ℕy:ℕx✝:[1, x, y, 7].length = 3 + 1hsum:∀ x_1 ∈ [1, x, y, 7], x_1 ≠ 1 → ∃ y_1 ∈ [1, x, y, 7], ∃ z ∈ [1, x, y, 7], x_1 = y_1 + zhsorted:(1 < x ∧ 1 < y ∧ 1 < 7) ∧ (x < y ∧ x < 7) ∧ y < 7 ∧ ∀ (a' : ℕ), False → 7 < a'⊢ False
c:List ℕhlen:c.length = 3 + 1x:ℕy:ℕx✝:[1, x, y, 7].length = 3 + 1hsum:∀ x_1 ∈ [1, x, y, 7], x_1 ≠ 1 → ∃ y_1 ∈ [1, x, y, 7], ∃ z ∈ [1, x, y, 7], x_1 = y_1 + zh1x:1 < xh1y:1 < yhxy:x < yhx7:x < 7hy7:y < 7⊢ False
c:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 2, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 2, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 2, y, 7], ∃ z ∈ [1, 2, y, 7], x = y_1 + zh1x:1 < 2hxy:2 < yhx7:2 < 7⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 3, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 3, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 3, y, 7], ∃ z ∈ [1, 3, y, 7], x = y_1 + zh1x:1 < 3hxy:3 < yhx7:3 < 7⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 4, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 4, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 4, y, 7], ∃ z ∈ [1, 4, y, 7], x = y_1 + zh1x:1 < 4hxy:4 < yhx7:4 < 7⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 5, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 5, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 5, y, 7], ∃ z ∈ [1, 5, y, 7], x = y_1 + zh1x:1 < 5hxy:5 < yhx7:5 < 7⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 6, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 6, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 6, y, 7], ∃ z ∈ [1, 6, y, 7], x = y_1 + zh1x:1 < 6hxy:6 < yhx7:6 < 7⊢ False c:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 2, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 2, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 2, y, 7], ∃ z ∈ [1, 2, y, 7], x = y_1 + zh1x:1 < 2hxy:2 < yhx7:2 < 7⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 3, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 3, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 3, y, 7], ∃ z ∈ [1, 3, y, 7], x = y_1 + zh1x:1 < 3hxy:3 < yhx7:3 < 7⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 4, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 4, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 4, y, 7], ∃ z ∈ [1, 4, y, 7], x = y_1 + zh1x:1 < 4hxy:4 < yhx7:4 < 7⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 5, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 5, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 5, y, 7], ∃ z ∈ [1, 5, y, 7], x = y_1 + zh1x:1 < 5hxy:5 < yhx7:5 < 7⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1y:1 < yhy7:y < 7x✝:[1, 6, y, 7].length = 3 + 1hsum:∀ x ∈ [1, 6, y, 7], x ≠ 1 → ∃ y_1 ∈ [1, 6, y, 7], ∃ z ∈ [1, 6, y, 7], x = y_1 + zh1x:1 < 6hxy:6 < yhx7:6 < 7⊢ False All goals completed! 🐙 c:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 2hx7:2 < 7h1y:1 < 3hy7:3 < 7x✝:[1, 2, 3, 7].length = 3 + 1hsum:∀ x ∈ [1, 2, 3, 7], x ≠ 1 → ∃ y ∈ [1, 2, 3, 7], ∃ z ∈ [1, 2, 3, 7], x = y + zhxy:2 < 3⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 2hx7:2 < 7h1y:1 < 4hy7:4 < 7x✝:[1, 2, 4, 7].length = 3 + 1hsum:∀ x ∈ [1, 2, 4, 7], x ≠ 1 → ∃ y ∈ [1, 2, 4, 7], ∃ z ∈ [1, 2, 4, 7], x = y + zhxy:2 < 4⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 2hx7:2 < 7h1y:1 < 5hy7:5 < 7x✝:[1, 2, 5, 7].length = 3 + 1hsum:∀ x ∈ [1, 2, 5, 7], x ≠ 1 → ∃ y ∈ [1, 2, 5, 7], ∃ z ∈ [1, 2, 5, 7], x = y + zhxy:2 < 5⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 2hx7:2 < 7h1y:1 < 6hy7:6 < 7x✝:[1, 2, 6, 7].length = 3 + 1hsum:∀ x ∈ [1, 2, 6, 7], x ≠ 1 → ∃ y ∈ [1, 2, 6, 7], ∃ z ∈ [1, 2, 6, 7], x = y + zhxy:2 < 6⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 3hx7:3 < 7h1y:1 < 4hy7:4 < 7x✝:[1, 3, 4, 7].length = 3 + 1hsum:∀ x ∈ [1, 3, 4, 7], x ≠ 1 → ∃ y ∈ [1, 3, 4, 7], ∃ z ∈ [1, 3, 4, 7], x = y + zhxy:3 < 4⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 3hx7:3 < 7h1y:1 < 5hy7:5 < 7x✝:[1, 3, 5, 7].length = 3 + 1hsum:∀ x ∈ [1, 3, 5, 7], x ≠ 1 → ∃ y ∈ [1, 3, 5, 7], ∃ z ∈ [1, 3, 5, 7], x = y + zhxy:3 < 5⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 3hx7:3 < 7h1y:1 < 6hy7:6 < 7x✝:[1, 3, 6, 7].length = 3 + 1hsum:∀ x ∈ [1, 3, 6, 7], x ≠ 1 → ∃ y ∈ [1, 3, 6, 7], ∃ z ∈ [1, 3, 6, 7], x = y + zhxy:3 < 6⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 4hx7:4 < 7h1y:1 < 5hy7:5 < 7x✝:[1, 4, 5, 7].length = 3 + 1hsum:∀ x ∈ [1, 4, 5, 7], x ≠ 1 → ∃ y ∈ [1, 4, 5, 7], ∃ z ∈ [1, 4, 5, 7], x = y + zhxy:4 < 5⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 4hx7:4 < 7h1y:1 < 6hy7:6 < 7x✝:[1, 4, 6, 7].length = 3 + 1hsum:∀ x ∈ [1, 4, 6, 7], x ≠ 1 → ∃ y ∈ [1, 4, 6, 7], ∃ z ∈ [1, 4, 6, 7], x = y + zhxy:4 < 6⊢ Falsec:List ℕhlen:c.length = 3 + 1x:ℕy:ℕh1x:1 < 5hx7:5 < 7h1y:1 < 6hy7:6 < 7x✝:[1, 5, 6, 7].length = 3 + 1hsum:∀ x ∈ [1, 5, 6, 7], x ≠ 1 → ∃ y ∈ [1, 5, 6, 7], ∃ z ∈ [1, 5, 6, 7], x = y + zhxy:5 < 6⊢ False All goals completed! 🐙The first few values of $\ell(n)$. See OEIS A003313.
All goals completed! 🐙end ScholzConjecture