Submission Details

Back to Submissions List

Challenge: Two, but not four

Submitted by: ansar

Submitted at: 2025-05-10 21:31:15

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
  · simp [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.pow_mod]
  · simp [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, pow_mul, Nat.pow_mod]

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmpo4xr3jl7/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/tmpo4xr3jl7/proof.olean
Finished imports
Finished replay
---
theorem
temp.tmpo4xr3jl7.proof._auxLemma.1
∀ {m n : ℕ}, (m ∣ n) = (n % m = 0)
#[propext]
---
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]
Finished with no errors.