Leap year theorem: The proof via Lean4.

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

$\gcd(x,80) > \gcd(x,50)$

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:

$\gcd(x,80) > \gcd(x,50) \implies x \text{ is a leap year}.$

Here "leap year" means the Gregorian rule:

$4 \mid x \land (100 \mid x \to 400 \mid x).$

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 $x$ is not divisible by $4$ , then we will show

$\gcd(x,80) \leq \gcd(x,50).$

Second, if $x$ is divisible by $100$ but not by $400$ , then again we will show

$\gcd(x,80) \leq \gcd(x,50).$

Both conclusions contradict the assumption

$\gcd(x,80) > \gcd(x,50).$

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 $100 \mid x$ but $400 \nmid x$ . Since $100 \mid x$ , we also have $50 \mid x$ , hence

$\gcd(x,50)=50.$

It remains to show that $\gcd(x,80)\leq 50$ . Let

$d=\gcd(x,80).$

Then $d\mid x$ and $d\mid 80$ . If $d=80$ , then $80\mid x$ . Together with $100\mid x$ , this implies

$\operatorname{lcm}(80,100)=400 \mid x,$

contradicting the assumption $400\nmid x$ . Therefore the only possible divisor of $80$ larger than $50$ , namely $80$ , is impossible. Thus $d\leq 50$ .

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 $4\nmid x$ , and let

$d=\gcd(x,80).$

Then $d\mid x$ and $d\mid 80$ . Since $4\nmid x$ , we cannot have $4\mid d$ , because $d\mid x$ would then imply $4\mid x$ .

Therefore $d$ is a divisor of

$80 = 2^4\cdot 5$

which is not divisible by $4$ . The only such divisors are

$1,2,5,10.$

Each of these divides $50$ . Hence

$d \mid 50.$

Since also $d\mid x$ , it follows that

$d \mid \gcd(x,50).$

Therefore

$\gcd(x,80) \leq \gcd(x,50).$

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:

$\gcd(x,80) > \gcd(x,50) \implies x \text{ is a Gregorian leap year}.$