Submission Details

Back to Submissions List

Challenge: Two, but not four

Submitted by: ansar

Submitted at: 2025-05-10 21:30:06

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

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmp60p0utn_/proof.lean:
/root/CodeProofTheArena/temp/tmp60p0utn_/proof.lean:6:11: warning: unused variable `n`
note: this linter can be disabled with `set_option linter.unusedVariables false`
/root/CodeProofTheArena/temp/tmp60p0utn_/proof.lean:11:3: error: unsolved goals
case left
n : ℕ
⊢ 2 ∣ 3 ^ (2 * n) + 1

case right
n : ℕ
⊢ ¬4 ∣ 3 ^ (2 * n) + 1
/root/CodeProofTheArena/temp/tmp60p0utn_/proof.lean:13:2: error: unexpected token '·'; expected command