75792.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

22 declarations, 2 contain sorry, 0 declared as axioms

Mathoverflow 75792

Various questions about integer complexity, which is the minimum number of 1s needed to express a natural number using addition, multiplication, and parentheses.

Let ‖n‖ denote the integer complexity of n > 0.

It is known that ‖3^n‖ = 3n for n > 0.
Is it true that ‖2^n‖ = 2n for n > 0?
The corresponding conjecture for 5 is false, because 5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)!

We have chosen to formalise this using an inductive type.

References:

mathoverflow/75792 by user Harry Altman
http://arxiv.org/abs/1203.6462 by Jānis Iraids, Kaspars Balodis, Juris Čerņenoks, Mārtiņš Opmanis, Rihards Opmanis, Kārlis Podnieks
http://arxiv.org/abs/1207.4841 by Harry Altman, Joshua Zelinsky
https://oeis.org/A5245 : Mahler-Popken complexity.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

inductive Mathoverflow75792.Reachable The inductively defined predicate that m is reachable in n steps line 45 source

Source documentation

The inductively defined predicate that m is reachable in n steps.

no axioms what this means

Statement uses: Nat

inductive Reachable : ℕ → ℕ → Prop
  | one : Reachable 1 1
  | add {m n a b} : Reachable m a → Reachable n b → Reachable (m + n) (a + b)
  | mul {m n a b} : Reachable m a → Reachable n b → Reachable (m * n) (a + b)

@[category test, AMS 11]

Mentions: test, AMS

theorem Mathoverflow75792.Reachable.self line 51 source
no axioms what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Mathoverflow75792.Reachable
Proof uses: Nat.le_induction, Nat.succ, Mathoverflow75792.Reachable.one, LE.le, Mathoverflow75792.Reachable.add
5 instances, coercions and auxiliary constants left out.
theorem Mathoverflow75792.not_reachable_zero_fst line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Mathoverflow75792.Reachable, OfNat.ofNat
Proof uses: Mathoverflow75792.Reachable.rec, Eq, False, absurd, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, HAdd.hAdd, False.elim, Eq.mp, Eq.trans, True, implies_congr, congrArg, And, propext, add_eq_zero and 8 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.not_reachable_zero_snd line 62 source
standard axioms: propext what this means
Statement uses: Nat, Not, Mathoverflow75792.Reachable, OfNat.ofNat
Proof uses: Mathoverflow75792.Reachable.rec, Eq, False, absurd, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, HAdd.hAdd, False.elim, Eq.mp, Eq.trans, True, implies_congr, congrArg, And, propext, add_eq_zero and 4 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.Reachable.dec line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Mathoverflow75792.Reachable, Exists, And, Eq, HAdd.hAdd, OfNat.ofNat
Proof uses: Nat.casesAuxOn, absurd, Mathoverflow75792.not_reachable_zero_fst, Mathoverflow75792.not_reachable_zero_snd, Exists.intro, And.intro, rfl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.Reachable.le line 78 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, Mathoverflow75792.Reachable
Proof uses: Nat.le.rec, Nat.le, Eq.mpr, Nat.succ, HMul.hMul, OfNat.ofNat, HAdd.hAdd, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true, Eq.trans, True, congrArg, mul_one, eq_self, Mathoverflow75792.Reachable.mul and 1 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.reachable_iff_of_two_le line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Iff, Mathoverflow75792.Reachable, Exists, LT.lt, And, Eq, HAdd.hAdd, Or, HMul.hMul
Proof uses: Iff.intro, Mathoverflow75792.Reachable.rec, absurd, of_decide_eq_true, Not, id, Bool, Decidable.decide, Bool.true, Eq.refl, Mathoverflow75792.Reachable.dec, Exists.intro, Decidable.byContradiction, And.intro, rfl, Or.inl, Nat.casesAuxOn, Eq.mpr, congrArg, Eq.symm and 19 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
def Mathoverflow75792.Reachable.decAux Auxiliary decision procedure for Reachable, taking a fuel argument f bounding m line 116 source
Source documentation
Auxiliary decision procedure for Reachable, taking a fuel argument f bounding m.
reachable_iff_of_two_le reduces Reachable m n for 2 ≤ m to statements Reachable m' n' with m' < m, so one unit of fuel per unit of m always suffices. Recursing on the fuel rather than on m makes this structural, so Reachable.decide below avoids well-founded recursion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Decidable, Mathoverflow75792.Reachable
4 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
def Reachable.decAux : ∀ (f m n : ℕ), m ≤ f → Decidable (Reachable m n)
  |     _,     0,     n,  _ => isFalse (not_reachable_zero_fst n)
  |     _,     1,     0,  _ => isFalse (not_reachable_zero_snd 1)
  |     _,     1, _ + 1,  _ => isTrue (Reachable.one.le (by lia))
  |     0, _ + 2,     _, hf => absurd hf (by lia)
  | f + 1, m + 2,     n, hf => by
      let d : ∀ {m₁} (h : m₁ < m + 2) {n}, Decidable (Reachable m₁ n) :=
…
```
Mentions: Mathoverflow75792.Reachable, Mathoverflow75792.not_reachable_zero_fst, Mathoverflow75792.not_reachable_zero_snd
instance Mathoverflow75792.Reachable.decide line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Decidable, Mathoverflow75792.Reachable
Proof uses: Mathoverflow75792.Reachable.decAux, le_rfl
1 instances, coercions and auxiliary constants left out.
def Mathoverflow75792.complexity The (Mahler-Popken) complexity of n: the minimum number of 1s needed to express a given number using only addition and multiplication line 141 source
Source documentation
The (Mahler-Popken) complexity of n: the minimum number of 1s needed to express a given number using only addition and multiplication. E.g. 2 = 1 + 1, so complexity 2 = 2.

L4DEL explanation
The (Mahler-Popken) complexity of n: the minimum number of 1s needed to express a given number using only addition and multiplication. E.g. 2 = 1 + 1, so complexity 2 = 2.
Sources and attribution: Pinned Lean source (1646ca16afd6)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: dite, Eq, OfNat.ofNat, Not, Nat.find, Mathoverflow75792.Reachable
4 instances, coercions and auxiliary constants left out.
```
def complexity (n : ℕ) : ℕ :=
…
```
theorem Mathoverflow75792.Reachable.complexity_le line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Mathoverflow75792.Reachable, LE.le, Mathoverflow75792.complexity
Proof uses: id, dite, Eq, OfNat.ofNat, Not, Nat.find, Eq.mpr, congrFun', congrArg, dif_pos, absurd, Mathoverflow75792.not_reachable_zero_fst, Eq.symm, dif_neg, Nat.find_min'
7 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.Reachable.complexity_eq line 152 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Mathoverflow75792.Reachable, LT.lt, Not, Eq, Mathoverflow75792.complexity
Proof uses: le_antisymm, Mathoverflow75792.Reachable.complexity_le, id, LE.le, dite, OfNat.ofNat, Nat.find, Eq.mpr, congrArg, dif_pos, absurd, Mathoverflow75792.not_reachable_zero_fst, Eq.symm, dif_neg, Iff.mpr, Nat.le_find_iff
11 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.Reachable.complexity line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Mathoverflow75792.Reachable, Mathoverflow75792.complexity
Proof uses: id, Eq.mpr, dite, Eq, Not, Nat.find, ne_of_gt, congrArg, dif_neg, Nat.find_spec
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.complexity_zero line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Mathoverflow75792.complexity, OfNat.ofNat
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
theorem Mathoverflow75792.complexity_one line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Mathoverflow75792.complexity, OfNat.ofNat
Proof uses: Mathoverflow75792.Reachable.complexity_eq, Mathoverflow75792.Reachable.one, LT.lt, Decidable.byContradiction, Not, Mathoverflow75792.Reachable, Mathoverflow75792.not_reachable_zero_snd, Eq.symm
6 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.complexity_two line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Mathoverflow75792.complexity, OfNat.ofNat
Proof uses: Mathoverflow75792.Reachable.complexity_eq, HAdd.hAdd, Mathoverflow75792.Reachable.add, Mathoverflow75792.Reachable.one, LT.lt, dite, Not, Mathoverflow75792.Reachable, LE.le, Eq.mpr, Exists, And, Or, HMul.hMul, id, congrArg, propext, Mathoverflow75792.reachable_iff_of_two_le, Decidable.byContradiction, False and 11 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.Reachable.pow line 185 source
standard axioms: propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Mathoverflow75792.Reachable, HPow.hPow, HMul.hMul
Proof uses: Nat.le.rec, Nat.succ, Eq.mpr, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true, Eq.trans, True, congrFun', congrArg, zero_add, pow_one, eq_self, mul_one, Mathoverflow75792.Reachable.self, Nat.le and 3 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow75792.Reachable.pow' line 191 source
standard axioms: propext what this means
Statement uses: PNat, Mathoverflow75792.Reachable, HPow.hPow, Nat, HMul.hMul
Proof uses: Mathoverflow75792.Reachable.pow, PNat.pos
8 instances, coercions and auxiliary constants left out.
theorem Mathoverflow75792.Reachable.five_pow_six 5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)! line 196 source
Source documentation
5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)!

standard axioms: propext what this means
Statement uses: Mathoverflow75792.Reachable, HPow.hPow, Nat, OfNat.ofNat
Proof uses: Mathoverflow75792.Reachable.pow', PNat, Mathoverflow75792.Reachable.add, HMul.hMul, HAdd.hAdd, Mathoverflow75792.Reachable.one, Mathoverflow75792.Reachable.mul
12 instances, coercions and auxiliary constants left out.
```
theorem Reachable.five_pow_six : Reachable (5^6) 29 :=
…
```
Mentions: Mathoverflow75792.Reachable
theorem Mathoverflow75792.complexity_five_pow Is 5n the complexity of 5^n for 0 < n? line 204 source
Source documentation
Is 5n the complexity of 5^n for 0 < n? Answer: No.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, Nat, LT.lt, OfNat.ofNat, Eq, Mathoverflow75792.complexity, HPow.hPow, HMul.hMul
Proof uses: id, Eq.mpr, Exists, And, Not, Eq.trans, false_iff, congrArg, funext, Exists.intro, And.intro, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, absurd, LE.le, Eq.rec, Mathoverflow75792.Reachable.complexity_le and 1 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem complexity_five_pow : answer(False) ↔ ∀ n : ℕ, 0 < n → complexity (5 ^ n) = 5 * n := by
…
```
Mentions: Mathoverflow75792.complexity
theorem Mathoverflow75792.complexity_three_pow Is 3n the complexity of 3^n for 0 < n? sorry line 214 source
Source documentation
Is 3n the complexity of 3^n for 0 < n? Answer: Yes, by John Selfridge.
Reference: https://arxiv.org/abs/1207.4841

depends on sorry what this means
Statement uses: Iff, True, Nat, LT.lt, OfNat.ofNat, Eq, Mathoverflow75792.complexity, HPow.hPow, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem complexity_three_pow : answer(True) ↔ ∀ n : ℕ, 0 < n → complexity (3 ^ n) = 3 * n := by
…
```
Mentions: Mathoverflow75792.complexity
theorem Mathoverflow75792.complexity_two_pow Is 2n the complexity of 2^n for 0 < n? sorry line 219 source
Source documentation
Is 2n the complexity of 2^n for 0 < n?

depends on sorry what this means
Statement uses: Iff, True, Nat, LT.lt, OfNat.ofNat, Eq, Mathoverflow75792.complexity, HPow.hPow, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem complexity_two_pow : answer(sorry) ↔ ∀ n : ℕ, 0 < n → complexity (2 ^ n) = 2 * n := by
…
```
Mentions: Mathoverflow75792.complexity