Leap year theorem: The proof via Lean4.

Back in July of 2021 I wrote a blog post that claimed a relationship between the inequality

[math]

and the Gregorian leap-year rule. More than five years later, a couple of experiences wiser and with some proof assistant advancements available, I decided to formally verify the core claim of that blog post, namely:

[math]

Here "leap year" means the Gregorian rule:

[math]

In Lean4, we can formalise this as follows. We start by defining the predicate LeapYear on natural numbers:

import Mathlib
/--
  Gregorian leap-year rule:
  a year is leap iff it is divisible by 4, and if it is divisible by 100,
  then it is also divisible by 400.
-/
def LeapYear (x : ℕ) : Prop :=
  4 ∣ x ∧ (100 ∣ x → 400 ∣ x)

The proof splits into the two ways in which a year can fail to be a Gregorian leap year.

First, if [math] is not divisible by [math], then we will show

[math]

Second, if [math] is divisible by [math] but not by [math], then again we will show

[math]

Both conclusions contradict the assumption

[math]

The main theorem then has the following shape.

private lemma gcd80_le_gcd50_of_not_four_dvd {x : ℕ} (hx : ¬ 4 ∣ x) :
    Nat.gcd x 80 ≤ Nat.gcd x 50 := by
  sorry
private lemma gcd80_le_gcd50_of_100_dvd_not_400_dvd {x : ℕ}
    (h100 : 100 ∣ x) (h400 : ¬ 400 ∣ x) :
    Nat.gcd x 80 ≤ Nat.gcd x 50 := by
  sorry
theorem leapYear_of_gcd80_gt_gcd50 {x : ℕ}
    (h : Nat.gcd x 80 > Nat.gcd x 50) :
    LeapYear x := by
  constructor
  · by_contra hx
    have hle := gcd80_le_gcd50_of_not_four_dvd hx
    exact (not_lt_of_ge hle) h
  · intro h100
    by_contra h400
    have hle := gcd80_le_gcd50_of_100_dvd_not_400_dvd h100 h400
    exact (not_lt_of_ge hle) h

Now we prove the two helper lemmas.

For the second helper lemma, suppose [math] but [math]. Since [math], we also have [math], hence

[math]

It remains to show that [math]. Let

[math]

Then [math] and [math]. If [math], then [math]. Together with [math], this implies

[math]

contradicting the assumption [math]. Therefore the only possible divisor of [math] larger than [math], namely [math], is impossible. Thus [math].

private lemma gcd80_le_gcd50_of_100_dvd_not_400_dvd {x : ℕ}
    (h100 : 100 ∣ x) (h400 : ¬ 400 ∣ x) :
    Nat.gcd x 80 ≤ Nat.gcd x 50 := by
  have h50 : 50 ∣ x := dvd_trans (by decide : 50 ∣ 100) h100
  have hg50 : Nat.gcd x 50 = 50 := by
    exact Nat.dvd_antisymm
      (Nat.gcd_dvd_right x 50)
      (Nat.dvd_gcd h50 dvd_rfl)
  rw [hg50]
  let d := Nat.gcd x 80
  have hdx : d ∣ x := Nat.gcd_dvd_left x 80
  have hd80 : d ∣ 80 := Nat.gcd_dvd_right x 80
  have hle80 : d ≤ 80 := Nat.le_of_dvd (by decide : 0 < 80) hd80
  change d ≤ 50
  interval_cases d <;> simp at hd80 ⊢
  all_goals
    exfalso
    apply h400
    have h80 : 80 ∣ x := by
      simpa using hdx
    have hlcm : Nat.lcm 80 100 ∣ x := Nat.lcm_dvd h80 h100
    rw [show Nat.lcm 80 100 = 400 by native_decide] at hlcm
    exact hlcm

For the first helper lemma, suppose [math], and let

[math]

Then [math] and [math]. Since [math], we cannot have [math], because [math] would then imply [math].

Therefore [math] is a divisor of

[math]

which is not divisible by [math]. The only such divisors are

[math]

Each of these divides [math]. Hence

[math]

Since also [math], it follows that

[math]

Therefore

[math]

In Lean, I chose to first prove the stronger divisibility statement.

private lemma gcd80_dvd50_of_not_four_dvd {x : ℕ} (hx : ¬ 4 ∣ x) :
    Nat.gcd x 80 ∣ 50 := by
  let d := Nat.gcd x 80
  have hdx : d ∣ x := Nat.gcd_dvd_left x 80
  have hd80 : d ∣ 80 := Nat.gcd_dvd_right x 80
  have hle80 : d ≤ 80 := Nat.le_of_dvd (by decide : 0 < 80) hd80
  change d ∣ 50
  interval_cases d <;> simp at hd80 ⊢
  all_goals
    exfalso
    apply hx
    exact dvd_trans (by decide) hdx
private lemma gcd80_le_gcd50_of_not_four_dvd {x : ℕ} (hx : ¬ 4 ∣ x) :
    Nat.gcd x 80 ≤ Nat.gcd x 50 := by
  exact Nat.le_of_dvd
    (Nat.gcd_pos_of_pos_right x (by decide : 0 < 50))
    (Nat.dvd_gcd
      (Nat.gcd_dvd_left x 80)
      (gcd80_dvd50_of_not_four_dvd hx))

Combining the two helper lemmas gives the desired implication.

theorem leapYear_of_gcd80_gt_gcd50 {x : ℕ}
    (h : Nat.gcd x 80 > Nat.gcd x 50) :
    LeapYear x := by
  constructor
  · by_contra hx
    have hle := gcd80_le_gcd50_of_not_four_dvd hx
    exact (not_lt_of_ge hle) h
  · intro h100
    by_contra h400
    have hle := gcd80_le_gcd50_of_100_dvd_not_400_dvd h100 h400
    exact (not_lt_of_ge hle) h

Thus we have formally proved:

[math]