1. FormalConjectures
  2. Mathoverflow
  3. «75792»
/- Copyright 2025 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 FormalConjecturesUtil

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.

namespace Mathoverflow75792

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

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] theorem Reachable.self (n : ℕ) (hn : 0 < n) : Reachable n n := Nat.le_induction .one (fun _ _ ih ↦ .add ih .one) n hnn:ℕm:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = m✝ → Falsea_ih✝:0 = n✝ → Falsehm:m✝ = 0 ∨ n✝ = 0⊢ False; All goals completed! 🐙m:ℕn:ℕm✝:ℕn✝:ℕa✝:ℕb✝:ℕh₁:Reachable m✝ a✝h₂:Reachable n✝ b✝a_ih✝¹:0 = a✝ → Falsea_ih✝:0 = b✝ → Falsehn:a✝ = 0 ∧ b✝ = 0⊢ False; All goals completed! 🐙@[category test, AMS 11] theorem Reachable.dec {m n : ℕ} (h : Reachable m n) : ∃ m' n', m' + 1 = m ∧ n' + 1 = n := m:ℕn:ℕh:Reachable m n⊢ ∃ m' n', m' + 1 = m ∧ n' + 1 = n n:ℕh:Reachable 0 n⊢ ∃ m' n', m' + 1 = 0 ∧ n' + 1 = nn:ℕm:ℕh:Reachable (m + 1) n⊢ ∃ m' n', m' + 1 = m + 1 ∧ n' + 1 = n n:ℕh:Reachable 0 n⊢ ∃ m' n', m' + 1 = 0 ∧ n' + 1 = n All goals completed! 🐙 m:ℕh:Reachable (m + 1) 0⊢ ∃ m' n', m' + 1 = m + 1 ∧ n' + 1 = 0m:ℕn:ℕh:Reachable (m + 1) (n + 1)⊢ ∃ m' n', m' + 1 = m + 1 ∧ n' + 1 = n + 1 m:ℕh:Reachable (m + 1) 0⊢ ∃ m' n', m' + 1 = m + 1 ∧ n' + 1 = 0 All goals completed! 🐙 All goals completed! 🐙@[category test, AMS 11] theorem Reachable.le {m n₁ n₂ : ℕ} (hn : n₁ ≤ n₂) (hm : Reachable m n₁) : Reachable m n₂ := m:ℕn₁:ℕn₂:ℕhn:n₁ ≤ n₂hm:Reachable m n₁⊢ Reachable m n₂ induction hn with m:ℕn₁:ℕn₂:ℕhm:Reachable m n₁⊢ Reachable m n₁ All goals completed! 🐙 m:ℕn₁:ℕn₂:ℕhm:Reachable m n₁m✝:ℕh:n₁.le m✝ih:Reachable m m✝⊢ Reachable m m✝.succ m:ℕn₁:ℕn₂:ℕhm:Reachable m n₁m✝:ℕh:n₁.le m✝ih:Reachable m m✝⊢ m = m * 1; All goals completed! 🐙m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)h₂:Reachable (0 + 1) (n₄ + 1)ih₂:2 ≤ 0 + 1 → ∃ m₁, ∃ (_ : m₁ < 0 + 1), ∃ m₂, ∃ (_ : m₂ < 0 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 0 + 1 ∨ m₁ * m₂ = 0 + 1)hm:2 ≤ (m₃ + 1 + 1) * (0 + 1)m₅:ℕhm₅:m₅ < m₃ + 1 + 1m₆:ℕhm₆:m₆ < m₃ + 1 + 1n₅:ℕhn₅:n₅ < n₃ + 1n₆:ℕhn₆:n₆ < n₃ + 1h₃:n₅ + n₆ = n₃ + 1h₄:Reachable m₅ n₅h₅:Reachable m₆ n₆h₆:m₅ + m₆ = m₃ + 1 + 1 ∨ m₅ * m₆ = m₃ + 1 + 1⊢ n₅ + (n₆ + n₄ + 1) = n₅ + n₆ + (n₄ + 1); All goals completed! 🐙, h₄, h₅.le ?_, ?_⟩ all_goals All goals completed! 🐙 m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ m₃ + 2 < (m₃ + 1 + 1) * (m₄ + 1 + 1)m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ m₄ + 2 < (m₃ + 1 + 1) * (m₄ + 1 + 1)m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ n₃ + 1 < n₃ + 1 + (n₄ + 1)m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ n₄ + 1 < n₃ + 1 + (n₄ + 1) m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ m₃ + 2 < (m₃ + 1 + 1) * (m₄ + 1 + 1) m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 0 < m₃ + 2m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 1 < m₄ + 1 + 1 m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 0 < m₃ + 2m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 1 < m₄ + 1 + 1 All goals completed! 🐙 m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ m₄ + 2 < (m₃ + 1 + 1) * (m₄ + 1 + 1) m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 0 < m₄ + 2m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 1 < m₃ + 1 + 1 m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 0 < m₄ + 2m:ℕn:ℕn₃:ℕn₄:ℕm₃:ℕh₁:Reachable (m₃ + 1 + 1) (n₃ + 1)ih₁:2 ≤ m₃ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₃ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₃ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₃ + 1), ∃ n₂, ∃ (_ : n₂ < n₃ + 1), n₁ + n₂ = n₃ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₃ + 1 + 1 ∨ m₁ * m₂ = m₃ + 1 + 1)m₄:ℕh₂:Reachable (m₄ + 1 + 1) (n₄ + 1)ih₂:2 ≤ m₄ + 1 + 1 → ∃ m₁, ∃ (_ : m₁ < m₄ + 1 + 1), ∃ m₂, ∃ (_ : m₂ < m₄ + 1 + 1), ∃ n₁, ∃ (_ : n₁ < n₄ + 1), ∃ n₂, ∃ (_ : n₂ < n₄ + 1), n₁ + n₂ = n₄ + 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m₄ + 1 + 1 ∨ m₁ * m₂ = m₄ + 1 + 1)hm:2 ≤ (m₃ + 1 + 1) * (m₄ + 1 + 1)⊢ 1 < m₃ + 1 + 1 All goals completed! 🐙 all_goals All goals completed! 🐙

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.

f:ℕm:ℕn:ℕhf:m + 2 ≤ f + 1d:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} ↦ decAux f m₁ n ⋯⊢ Decidable (Reachable (m + 2) n) refine @decidable_of_iff' _ _ (reachable_iff_of_two_le (m+2) n (f:ℕm:ℕn:ℕhf:m + 2 ≤ f + 1d:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} ↦ decAux f m₁ n ⋯⊢ 2 ≤ m + 2 All goals completed! 🐙)) ?_ f:ℕm:ℕn:ℕhf:m + 2 ≤ f + 1d:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} ↦ decAux f m₁ n ⋯m₁:ℕhm₁:m₁ < m + 2⊢ Decidable (∃ m₂, ∃ (_ : m₂ < m + 2), ∃ n₁, ∃ (_ : n₁ < n), ∃ n₂, ∃ (_ : n₂ < n), n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) f:ℕm:ℕn:ℕhf:m + 2 ≤ f + 1d:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} ↦ decAux f m₁ n ⋯m₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2⊢ Decidable (∃ n₁, ∃ (_ : n₁ < n), ∃ n₂, ∃ (_ : n₂ < n), n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) f:ℕm:ℕn:ℕhf:m + 2 ≤ f + 1d:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} ↦ decAux f m₁ n ⋯m₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2n₁:ℕhn₁:n₁ < n⊢ Decidable (∃ n₂, ∃ (_ : n₂ < n), n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) f:ℕm:ℕn:ℕhf:m + 2 ≤ f + 1d:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} ↦ decAux f m₁ n ⋯m₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2n₁:ℕhn₁:n₁ < nn₂:ℕhn₂:n₂ < n⊢ Decidable (n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) f:ℕm:ℕn:ℕhf:m + 2 ≤ f + 1d:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} ↦ decAux f m₁ n ⋯m₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2n₁:ℕhn₁:n₁ < nn₂:ℕhn₂:n₂ < n⊢ Decidable (Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) f:ℕm:ℕn:ℕhf:m + 2 ≤ f + 1d:{m₁ : ℕ} → m₁ < m + 2 → {n : ℕ} → Decidable (Reachable m₁ n) := fun {m₁} h {n} ↦ decAux f m₁ n ⋯m₁:ℕhm₁:m₁ < m + 2m₂:ℕhm₂:m₂ < m + 2n₁:ℕhn₁:n₁ < nn₂:ℕhn₂:n₂ < n⊢ Decidable (Reachable m₂ n₂ ∧ (m₁ + m₂ = m + 2 ∨ m₁ * m₂ = m + 2)) All goals completed! 🐙 termination_by structural f => finstance Reachable.decide (m n : ℕ) : Decidable (Reachable m n) := Reachable.decAux m m n le_rfl

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.

def complexity (n : ℕ) : ℕ := if h : n = 0 then 0 else Nat.find ⟨n, Reachable.self n <| n.pos_of_ne_zero h⟩@[category test, AMS 11] theorem Reachable.complexity_le {m n : ℕ} (h : Reachable m n) : complexity m ≤ n := m:ℕn:ℕh:Reachable m n⊢ complexity m ≤ n m:ℕn:ℕh:Reachable m n⊢ (if h : m = 0 then 0 else Nat.find ⋯) ≤ n m:ℕn:ℕh:Reachable m nh':m = 0⊢ 0 ≤ nm:ℕn:ℕh:Reachable m nh':¬m = 0⊢ Nat.find ⋯ ≤ n m:ℕn:ℕh:Reachable m nh':m = 0⊢ 0 ≤ n n:ℕh:Reachable 0 n⊢ 0 ≤ n; All goals completed! 🐙 All goals completed! 🐙@[category test, AMS 11] theorem Reachable.complexity_eq {m n : ℕ} (h : Reachable m n) (min : ∀ n' < n, ¬ Reachable m n') : complexity m = n := m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'⊢ complexity m = n m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'⊢ n ≤ complexity m m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'⊢ n ≤ if h : m = 0 then 0 else Nat.find ⋯ m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'h':m = 0⊢ n ≤ 0m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'h':¬m = 0⊢ n ≤ Nat.find ⋯ m:ℕn:ℕh:Reachable m nmin:∀ n' < n, ¬Reachable m n'h':m = 0⊢ n ≤ 0 n:ℕh:Reachable 0 nmin:∀ n' < n, ¬Reachable 0 n'⊢ n ≤ 0; All goals completed! 🐙 All goals completed! 🐙n:ℕhn:0 < n⊢ Reachable n (Nat.find ⋯) All goals completed! 🐙@[category test, AMS 11] theorem complexity_zero : complexity 0 = 0 := rfln':ℕhn':n' < 1this:n' = 0⊢ ¬Reachable 1 n' hn':0 < 1⊢ ¬Reachable 1 0; All goals completed! 🐙n':ℕhn':1 < 1 + 1⊢ ¬∃ m₁, ∃ (_ : m₁ < 2), ∃ m₂, ∃ (_ : m₂ < 2), ∃ n₁, ∃ (_ : n₁ < 1), ∃ n₂, ∃ (_ : n₂ < 1), n₁ + n₂ = 1 ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = 2 ∨ m₁ * m₂ = 2) n':ℕhn':1 < 1 + 1m₁:ℕhm₁:m₁ < 2m₂:ℕhm₂:m₂ < 2n₁:ℕhn₁:n₁ < 1n₂:ℕhn₂:n₂ < 1h₁:n₁ + n₂ = 1⊢ False All goals completed! 🐙@[category test, AMS 11] theorem Reachable.pow (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : Reachable (m ^ n) (m * n) := m:ℕn:ℕhm:0 < mhn:0 < n⊢ Reachable (m ^ n) (m * n) induction hn with m:ℕn:ℕhm:0 < m⊢ Reachable (m ^ Nat.succ 0) (m * Nat.succ 0) m:ℕn:ℕhm:0 < m⊢ m ^ Nat.succ 0 = mm:ℕn:ℕhm:0 < m⊢ m * Nat.succ 0 = m m:ℕn:ℕhm:0 < m⊢ m ^ Nat.succ 0 = mm:ℕn:ℕhm:0 < m⊢ m * Nat.succ 0 = m All goals completed! 🐙 m:ℕn:ℕhm:0 < mm✝:ℕhn:(Nat.succ 0).le m✝ih:Reachable (m ^ m✝) (m * m✝)⊢ Reachable (m ^ m✝.succ) (m * m✝.succ) All goals completed! 🐙@[category test, AMS 11] theorem Reachable.pow' (m n : ℕ+) : Reachable (m ^ (n : ℕ) : ℕ) (m * n) := .pow _ _ m.pos n.pos

5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)!

@[category test, AMS 11] theorem Reachable.five_pow_six : Reachable (5^6) 29 := have h8 : Reachable 8 6 := .pow' 2 3 have h9 : Reachable 9 6 := .pow' 3 2 have h27 : Reachable 27 9 := .pow' 3 3 .add .one <| .mul h8 <| .mul h9 <| .add .one <| .mul h8 h27

Is 5n the complexity of 5^n for 0 < n? Answer: No.

@[category research solved, AMS 11] theorem complexity_five_pow : answer(False) ↔ ∀ n : ℕ, 0 < n → complexity (5 ^ n) = 5 * n := ⊢ False ↔ ∀ (n : ℕ), 0 < n → complexity (5 ^ n) = 5 * n ⊢ False ↔ ∀ (n : ℕ), 0 < n → complexity (5 ^ n) = 5 * n ⊢ ∃ x, 0 < x ∧ ¬complexity (5 ^ x) = 5 * x exact ⟨6, ⊢ 0 < 6 All goals completed! 🐙, fun h ↦ absurd (h ▸ Reachable.five_pow_six.complexity_le) (h:complexity (5 ^ 6) = 5 * 6⊢ ¬5 * 6 ≤ 29 All goals completed! 🐙)⟩

Is 3n the complexity of 3^n for 0 < n? Answer: Yes, by John Selfridge.

Reference: https://arxiv.org/abs/1207.4841

@[category research solved, AMS 11] theorem complexity_three_pow : answer(True) ↔ ∀ n : ℕ, 0 < n → complexity (3 ^ n) = 3 * n := ⊢ True ↔ ∀ (n : ℕ), 0 < n → complexity (3 ^ n) = 3 * n All goals completed! 🐙

Is 2n the complexity of 2^n for 0 < n?

@[category research open, AMS 11] theorem complexity_two_pow : answer(sorry) ↔ ∀ n : ℕ, 0 < n → complexity (2 ^ n) = 2 * n := ⊢ True ↔ ∀ (n : ℕ), 0 < n → complexity (2 ^ n) = 2 * n All goals completed! 🐙end Mathoverflow75792