Submission Details

Back to Submissions List

Challenge: minFac

Submitted by: Quang Dao

Submitted at: 2024-11-19 23:17:48

Code:

def minFac(a:Nat) (h: a>1): Nat 

:= Nat.find (p := fun x => x > 1 ∧ x ∣ a) ⟨a, And.intro h (Nat.dvd_refl a)⟩

First Theorem Proof:

theorem minFac_isfac(a:Nat)(h: a>1): ( (minFac a h) ∣a) ∧(minFac a h>1)

:= by
  simp [minFac]
  constructor
  · have := Nat.find_spec (p := fun x => x > 1 ∧ x ∣ a) ⟨a, And.intro h (Nat.dvd_refl a)⟩
    exact this.2
  · intro m hm hm'
    contrapose! hm'
    exact hm

Status: Incorrect

Feedback:

/tmp/tmpaa3u8hlr/proof.lean:7:54: error: expected token

Second Theorem Proof:

theorem minFac_ismin(a:Nat)(h:a>1): Not (∃ y>1,( y ∣ a) ∧y<minFac a h)

:= by
  simp [minFac]
  intro x hGt hDiv
  have := Nat.find_min' (p := fun x => x > 1 ∧ x ∣ a) ⟨a, And.intro h (Nat.dvd_refl a)⟩ (And.intro hGt hDiv)
  refine ⟨minFac a h, ?_⟩
  constructor
  · simp [this, minFac]
  · exact And.comm.mp (minFac_is_fac a h)

Status: Incorrect

Feedback:

/tmp/tmpaa3u8hlr/proof2.lean:8:58: error: expected token