Submission Details

Back to Submissions List

Challenge: Two, but not four

Submitted by: ansar

Submitted at: 2025-05-09 10:08:53

Code:

import Mathlib.Tactic

def dummy (n : ℕ) : ℕ

:= 0

First Theorem Proof:

theorem solution (n : ℕ) : 2 ∣ 3 ^ (2 * n) + 1 ∧ ¬ 4 ∣ (3 ^ (2 * n) + 1)

:= by
  constructor
  · rw [←even_iff_two_dvd, Nat.even_add_one, Nat.not_even_iff_odd]
    apply Odd.pow
    use 1
    rfl
  · have h : 4 ∣ 3 ^ (2 * n) - 1 := by
      have hsum : 3 ^ (2 * n) - 1 = (3 - 1) * ∑ i ∈ Finset.range (2 * n), 3 ^ i := by
        zify
        rw [Int.natCast_sub, Int.natCast_pow]
        symm
        ring_nf
        · have := mul_geom_sum (3 : ℤ) (2 * n)
          ring_nf at this
          exact this
        · apply Nat.one_le_pow
          linarith
      have : 2 ∣ ∑ i ∈ Finset.range (2 * n), 3 ^ i := by
        rw [Nat.dvd_iff_mod_eq_zero, Finset.sum_nat_mod]
        have (i : ℕ) : 3 ^ i % 2 = 1 := by
          rw [←Nat.odd_iff]
          apply Odd.pow
          use 1
          rfl
        simp [this]
      let ⟨k, hk⟩ := this
      clear this
      simp [hk, ←mul_assoc] at hsum
      use k
    let ⟨k, hk⟩ := h
    have : 3 ^ (2 * n) + 1 = 4 * k + 2 := by
      rw [←hk, ←Nat.sub_add_comm]
      · rw [Nat.add_sub_assoc]
        linarith
      · apply Nat.one_le_pow
        linarith
    rw [this, Nat.dvd_iff_mod_eq_zero, Nat.add_mod]
    clear this
    have : 4 * k % 4 = 0 := by
      rw [←Nat.dvd_iff_mod_eq_zero]
      use k
    rw [this, zero_add, Nat.mod_mod, ←Nat.dvd_iff_mod_eq_zero]
    apply Nat.not_dvd_of_pos_of_lt
    · linarith
    · linarith

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmpc1ddtjbu/target.olean
Finished imports
Finished replay
---
def
dummy
ℕ → ℕ
:= fun (n : Nat) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
solution
∀ (n : ℕ), 2 ∣ 3 ^ (2 * n) + 1 ∧ ¬4 ∣ 3 ^ (2 * n) + 1
#[propext, sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpc1ddtjbu/proof.olean
Finished imports
Finished replay
---
theorem
temp.tmpc1ddtjbu.proof._auxLemma.1
∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * (b * c) = a * b * c
#[]
---
def
solution.match_1
∀ (n : ℕ) (motive : 2 ∣ ∑ i ∈ Finset.range (2 * n), 3 ^ i → Prop) (this : 2 ∣ ∑ i ∈ Finset.range (2 * n), 3 ^ i),
  (∀ (k : ℕ) (hk : ∑ i ∈ Finset.range (2 * n), 3 ^ i = 2 * k), motive ⋯) → motive this
:= fun (n : Nat) (motive : (Dvd.dvd.{0} Nat Nat.instDvd (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (Finset.sum.{0, 0} Nat Nat Nat.instAddCommMonoid (Finset.range (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (fun (i : Nat) => HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) i))) -> Prop) (this._@.temp.tmpc1ddtjbu.proof._hyg.557 : Dvd.dvd.{0} Nat Nat.instDvd (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (Finset.sum.{0, 0} Nat Nat Nat.instAddCommMonoid (Finset.range (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (fun (i : Nat) => HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) i))) (h_1 : forall (k : Nat) (hk : Eq.{1} Nat (Finset.sum.{0, 0} Nat Nat Nat.instAddCommMonoid (Finset.range (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (fun (i : Nat) => HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) i)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) k)), motive (Exists.intro.{1} Nat (fun (c : Nat) => Eq.{1} Nat (Finset.sum.{0, 0} Nat Nat Nat.instAddCommMonoid (Finset.range (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (fun (i : Nat) => HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) i)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) c)) k hk)) => Exists.casesOn.{1} Nat (fun (c : Nat) => Eq.{1} Nat (Finset.sum.{0, 0} Nat Nat Nat.instAddCommMonoid (Finset.range (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (fun (i : Nat) => HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) i)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) c)) (fun (x : Dvd.dvd.{0} Nat Nat.instDvd (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (Finset.sum.{0, 0} Nat Nat Nat.instAddCommMonoid (Finset.range (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (fun (i : Nat) => HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) i))) => motive x) this._@.temp.tmpc1ddtjbu.proof._hyg.557 (fun (w._@.temp.tmpc1ddtjbu.proof._hyg.566 : Nat) (h._@.temp.tmpc1ddtjbu.proof._hyg.567 : Eq.{1} Nat (Finset.sum.{0, 0} Nat Nat Nat.instAddCommMonoid (Finset.range (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (fun (i : Nat) => HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) i)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) w._@.temp.tmpc1ddtjbu.proof._hyg.566)) => h_1 w._@.temp.tmpc1ddtjbu.proof._hyg.566 h._@.temp.tmpc1ddtjbu.proof._hyg.567)
#[propext, Quot.sound, Classical.choice]
---
def
dummy
ℕ → ℕ
:= fun (n : Nat) => OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)
#[]
---
theorem
solution
∀ (n : ℕ), 2 ∣ 3 ^ (2 * n) + 1 ∧ ¬4 ∣ 3 ^ (2 * n) + 1
#[propext, Quot.sound, Classical.choice]
---
def
solution.match_2
∀ (n : ℕ) (motive : 4 ∣ 3 ^ (2 * n) - 1 → Prop) (h : 4 ∣ 3 ^ (2 * n) - 1),
  (∀ (k : ℕ) (hk : 3 ^ (2 * n) - 1 = 4 * k), motive ⋯) → motive h
:= fun (n : Nat) (motive : (Dvd.dvd.{0} Nat Nat.instDvd (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> Prop) (h._@.temp.tmpc1ddtjbu.proof._hyg.606 : Dvd.dvd.{0} Nat Nat.instDvd (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) (h_1 : forall (k : Nat) (hk : Eq.{1} Nat (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) k)), motive (Exists.intro.{1} Nat (fun (c : Nat) => Eq.{1} Nat (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) c)) k hk)) => Exists.casesOn.{1} Nat (fun (c : Nat) => Eq.{1} Nat (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) c)) (fun (x : Dvd.dvd.{0} Nat Nat.instDvd (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) => motive x) h._@.temp.tmpc1ddtjbu.proof._hyg.606 (fun (w._@.temp.tmpc1ddtjbu.proof._hyg.615 : Nat) (h._@.temp.tmpc1ddtjbu.proof._hyg.616 : Eq.{1} Nat (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.toNatPow.{0} Nat Nat.instMonoid)) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) n)) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) (OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) w._@.temp.tmpc1ddtjbu.proof._hyg.615)) => h_1 w._@.temp.tmpc1ddtjbu.proof._hyg.615 h._@.temp.tmpc1ddtjbu.proof._hyg.616)
#[propext]
Finished with no errors.