Wikipedia · test · AMS 11
easyknown result, no worker yet
Scholz conjecture on addition chains
Exercise · additionChainLength_first_values
The first few values of . See OEIS A003313.
Formal statement · Lean 4.lean
theorem additionChainLength_first_values :
[ℓ(1), ℓ(2), ℓ(3), ℓ(4), ℓ(5), ℓ(6), ℓ(7), ℓ(8), ℓ(9), ℓ(10)] =
[0, 1, 2, 2, 3, 3, 4, 3, 4, 4] := by
sorryProof. sorry
Nobody has tried yet.