Submission Details

Back to Submissions List

Challenge: Two, but not four

Submitted by: ansar

Submitted at: 2025-05-09 09:19:26

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: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmp509m7h_s/target.lean:
/root/CodeProofTheArena/temp/tmp509m7h_s/target.lean:2:0: error: object file '././.lake/packages/mathlib/.lake/build/lib/Mathlib/Data/Nat/Basic.olean' of module Mathlib.Data.Nat.Basic does not exist