From 87ccd4f2419379491464509ced7037ee799c29e2 Mon Sep 17 00:00:00 2001 From: eyang07 <145517274+eyang07@users.noreply.github.com> Date: Wed, 1 Jul 2026 11:23:21 +0800 Subject: [PATCH 1/6] feat(Wikipedia): add Scholz conjecture on addition chains Formalise the Scholz conjecture from issue #2217. --- .../Wikipedia/ScholzConjecture.lean | 68 +++++++++++++++++++ 1 file changed, 68 insertions(+) create mode 100644 FormalConjectures/Wikipedia/ScholzConjecture.lean diff --git a/FormalConjectures/Wikipedia/ScholzConjecture.lean b/FormalConjectures/Wikipedia/ScholzConjecture.lean new file mode 100644 index 0000000000..f743da00a5 --- /dev/null +++ b/FormalConjectures/Wikipedia/ScholzConjecture.lean @@ -0,0 +1,68 @@ +/- +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 + +/-! +# Scholz conjecture on addition chains + +An *addition chain* for a positive integer `n` is a strictly increasing sequence +`1 = a₀ < a₁ < ⋯ < a_r = n` in which every entry after the first is the sum of two +(not necessarily distinct) earlier entries. The *length* `ℓ(n)` is the minimal number +of addition steps `r` over all such chains. + +The **Scholz conjecture** (also known as the Scholz–Brauer or Brauer–Scholz conjecture) +asserts that for every positive integer `n`, +$$\ell(2^n - 1) \le n - 1 + \ell(n).$$ + +*References:* +- [Wikipedia](https://en.wikipedia.org/wiki/Scholz_conjecture) +- [MathWorld](https://mathworld.wolfram.com/ScholzConjecture.html) +-/ + +namespace Scholz + +/-- `IsAdditionChain c` asserts that the list `c` is an addition chain: it starts at +`1`, is strictly increasing, and every entry after the first is the sum of two (not +necessarily distinct) earlier entries. The step condition is phrased with the safe +`getElem?` accessor: for each valid index `i ≠ 0` there are earlier indices `j, k` with +`c[i]? = c[j]? + c[k]?` (as `Option`-valued sums). -/ +def IsAdditionChain (c : List ℕ) : Prop := + c.head? = some 1 ∧ + c.Pairwise (· < ·) ∧ + ∀ i, i ≠ 0 → i < c.length → + ∃ j k, j < i ∧ k < i ∧ getElem? c i = (· + ·) <$> getElem? c j <*> getElem? c k + +/-- The length `ℓ(n)` of `n`: the minimal number of addition steps (number of entries +minus one) over all addition chains ending at `n`. -/ +noncomputable def additionChainLength (n : ℕ) : ℕ := + sInf { r | ∃ c : List ℕ, IsAdditionChain c ∧ c.getLast? = some n ∧ c.length = r + 1 } + +local notation "ℓ(" n ")" => additionChainLength n + +/-- +The 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)$. + +References: Wikipedia and MathWorld. +-/ +@[category research open, AMS 11 68] +theorem scholz_conjecture (n : ℕ) (hn : 0 < n) : + ℓ(2 ^ n - 1) ≤ n - 1 + ℓ(n) := by + sorry + +end Scholz From 8090b31b07090511d5aa2a2cce32edc00d3586c8 Mon Sep 17 00:00:00 2001 From: Eric <145517274+eyang07@users.noreply.github.com> Date: Sat, 4 Jul 2026 11:55:35 +0800 Subject: [PATCH 2/6] Update FormalConjectures/Wikipedia/ScholzConjecture.lean Co-authored-by: Jean-Guillaume Durand <113947520+jeangud@users.noreply.github.com> --- FormalConjectures/Wikipedia/ScholzConjecture.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/FormalConjectures/Wikipedia/ScholzConjecture.lean b/FormalConjectures/Wikipedia/ScholzConjecture.lean index f743da00a5..06dabb1fab 100644 --- a/FormalConjectures/Wikipedia/ScholzConjecture.lean +++ b/FormalConjectures/Wikipedia/ScholzConjecture.lean @@ -43,8 +43,7 @@ necessarily distinct) earlier entries. The step condition is phrased with the sa def IsAdditionChain (c : List ℕ) : Prop := c.head? = some 1 ∧ c.Pairwise (· < ·) ∧ - ∀ i, i ≠ 0 → i < c.length → - ∃ j k, j < i ∧ k < i ∧ getElem? c i = (· + ·) <$> getElem? c j <*> getElem? c k + ∀ x ∈ c, x ≠ 1 → ∃ y ∈ c, ∃ z ∈ c, x = y + z /-- The length `ℓ(n)` of `n`: the minimal number of addition steps (number of entries minus one) over all addition chains ending at `n`. -/ From 3b42272b8f6a9e49e582c706b31a0914a1c9d934 Mon Sep 17 00:00:00 2001 From: Eric <145517274+eyang07@users.noreply.github.com> Date: Sat, 4 Jul 2026 11:56:00 +0800 Subject: [PATCH 3/6] Update FormalConjectures/Wikipedia/ScholzConjecture.lean Co-authored-by: Jean-Guillaume Durand <113947520+jeangud@users.noreply.github.com> --- FormalConjectures/Wikipedia/ScholzConjecture.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/Wikipedia/ScholzConjecture.lean b/FormalConjectures/Wikipedia/ScholzConjecture.lean index 06dabb1fab..23243ba43f 100644 --- a/FormalConjectures/Wikipedia/ScholzConjecture.lean +++ b/FormalConjectures/Wikipedia/ScholzConjecture.lean @@ -33,7 +33,7 @@ $$\ell(2^n - 1) \le n - 1 + \ell(n).$$ - [MathWorld](https://mathworld.wolfram.com/ScholzConjecture.html) -/ -namespace Scholz +namespace ScholzConjecture /-- `IsAdditionChain c` asserts that the list `c` is an addition chain: it starts at `1`, is strictly increasing, and every entry after the first is the sum of two (not From 32a891887394f76a396ec32ddd2ad3e507cd1fd2 Mon Sep 17 00:00:00 2001 From: Eric <145517274+eyang07@users.noreply.github.com> Date: Sat, 4 Jul 2026 11:56:08 +0800 Subject: [PATCH 4/6] Update FormalConjectures/Wikipedia/ScholzConjecture.lean Co-authored-by: Jean-Guillaume Durand <113947520+jeangud@users.noreply.github.com> --- FormalConjectures/Wikipedia/ScholzConjecture.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/Wikipedia/ScholzConjecture.lean b/FormalConjectures/Wikipedia/ScholzConjecture.lean index 23243ba43f..8018a1dc54 100644 --- a/FormalConjectures/Wikipedia/ScholzConjecture.lean +++ b/FormalConjectures/Wikipedia/ScholzConjecture.lean @@ -64,4 +64,4 @@ theorem scholz_conjecture (n : ℕ) (hn : 0 < n) : ℓ(2 ^ n - 1) ≤ n - 1 + ℓ(n) := by sorry -end Scholz +end ScholzConjecture From 2e4876943789fcda51c24b5bc69418de27a58cb4 Mon Sep 17 00:00:00 2001 From: Eric <145517274+eyang07@users.noreply.github.com> Date: Sat, 4 Jul 2026 12:03:19 +0800 Subject: [PATCH 5/6] Update FormalConjectures/Wikipedia/ScholzConjecture.lean Co-authored-by: Jean-Guillaume Durand <113947520+jeangud@users.noreply.github.com> --- FormalConjectures/Wikipedia/ScholzConjecture.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/FormalConjectures/Wikipedia/ScholzConjecture.lean b/FormalConjectures/Wikipedia/ScholzConjecture.lean index 8018a1dc54..dd0d6760b7 100644 --- a/FormalConjectures/Wikipedia/ScholzConjecture.lean +++ b/FormalConjectures/Wikipedia/ScholzConjecture.lean @@ -56,8 +56,6 @@ local notation "ℓ(" n ")" => additionChainLength n The 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)$. - -References: Wikipedia and MathWorld. -/ @[category research open, AMS 11 68] theorem scholz_conjecture (n : ℕ) (hn : 0 < n) : From b7d260046496c911c1d814b8b80269fbee77ef73 Mon Sep 17 00:00:00 2001 From: eyang07 <145517274+eyang07@users.noreply.github.com> Date: Sat, 4 Jul 2026 12:40:44 +0800 Subject: [PATCH 6/6] Address review: LaTeX docstrings, dedupe statement, add reference - Use LaTeX syntax for math in docstrings - Drop the getElem? implementation note from IsAdditionChain's docstring - Remove the duplicated problem statement from the top-level docstring; reuse the addition-chain description on IsAdditionChain - Add the Tall (2022) reference (arXiv:2210.13812 / ePrint 2023/020) --- .../Wikipedia/ScholzConjecture.lean | 27 ++++++++----------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/FormalConjectures/Wikipedia/ScholzConjecture.lean b/FormalConjectures/Wikipedia/ScholzConjecture.lean index dd0d6760b7..30b512eb6e 100644 --- a/FormalConjectures/Wikipedia/ScholzConjecture.lean +++ b/FormalConjectures/Wikipedia/ScholzConjecture.lean @@ -19,34 +19,29 @@ import FormalConjectures.Util.ProblemImports /-! # Scholz conjecture on addition chains -An *addition chain* for a positive integer `n` is a strictly increasing sequence -`1 = a₀ < a₁ < ⋯ < a_r = n` in which every entry after the first is the sum of two -(not necessarily distinct) earlier entries. The *length* `ℓ(n)` is the minimal number -of addition steps `r` over all such chains. - -The **Scholz conjecture** (also known as the Scholz–Brauer or Brauer–Scholz conjecture) -asserts that for every positive integer `n`, -$$\ell(2^n - 1) \le n - 1 + \ell(n).$$ - *References:* - [Wikipedia](https://en.wikipedia.org/wiki/Scholz_conjecture) - [MathWorld](https://mathworld.wolfram.com/ScholzConjecture.html) +- [Tall22](https://arxiv.org/abs/2210.13812) 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](https://eprint.iacr.org/2023/020). -/ namespace ScholzConjecture -/-- `IsAdditionChain c` asserts that the list `c` is an addition chain: it starts at -`1`, is strictly increasing, and every entry after the first is the sum of two (not -necessarily distinct) earlier entries. The step condition is phrased with the safe -`getElem?` accessor: for each valid index `i ≠ 0` there are earlier indices `j, k` with -`c[i]? = c[j]? + c[k]?` (as `Option`-valued sums). -/ +/-- An *addition chain* is a strictly increasing sequence +$1 = a_0 < a_1 < \cdots < a_r$ in which every entry after the first is the sum of two +(not necessarily distinct) earlier entries. + +`IsAdditionChain c` asserts that the list $c$ is such a chain: it starts at $1$, is +strictly increasing, and every entry other than $1$ is a sum of two entries of $c$. -/ def IsAdditionChain (c : List ℕ) : Prop := c.head? = some 1 ∧ c.Pairwise (· < ·) ∧ ∀ x ∈ c, x ≠ 1 → ∃ y ∈ c, ∃ z ∈ c, x = y + z -/-- The length `ℓ(n)` of `n`: the minimal number of addition steps (number of entries -minus one) over all addition chains ending at `n`. -/ +/-- The *length* $\ell(n)$ of $n$: the minimal number of addition steps (the number of +entries minus one) over all addition chains ending at $n$. -/ noncomputable def additionChainLength (n : ℕ) : ℕ := sInf { r | ∃ c : List ℕ, IsAdditionChain c ∧ c.getLast? = some n ∧ c.length = r + 1 }