Last active
June 18, 2025 01:09
-
-
Save cmrfrd/abb7ce0c4086972eeb337fcf852acbc7 to your computer and use it in GitHub Desktop.
A lean4 proof showing there will always be at least 1 friday the thirteenth per year. Try in https://live.lean-lang.org/
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Mathlib.Data.ZMod.Basic | |
| import Mathlib.Data.Fin.Basic | |
| import Mathlib.Tactic.IntervalCases | |
| import Mathlib.Tactic | |
| import Mathlib.Tactic.FinCases | |
| import Mathlib.Data.Fintype.Basic | |
| import Mathlib.Data.Finset.Basic | |
| import Mathlib.Data.Finset.Card | |
| /-! | |
| # There Is Always a Friday the 13th | |
| proved by: Alex Comerford ([email protected]) | |
| This file is a small self‑contained Lean 4 proof of the classic fact that | |
| **every Gregorian calendar year contains at least one Friday whose date is the 13th**. | |
| The main argument is: Among the twelve months, each month’s 1st lands on some weekday. We | |
| also show via modulo residules that across a whole year every weekday (Monday, Tuesday, ...) | |
| shows up as a 1st, meaning that Sunday must occur as a 1st. Then by shifting 12 days, | |
| the 13th of that month must be a Friday. | |
| The inspiration for this proof came from: | |
| https://math.stackexchange.com/questions/59135/prove-that-every-year-has-at-least-one-friday-the-13th | |
| -/ | |
| set_option maxHeartbeats 10000000 | |
| open ZMod | |
| open Finset | |
| -- Defining the Gregorian calendar | |
| -- 0 = Jan, …, 11 = Dec | |
| abbrev Month := Fin 12 | |
| -- 0 = Sunday, 1 = Monday, ..., 6 = Saturday | |
| abbrev Weekday := ZMod 7 | |
| -- A leap year is a special year where we include an additional | |
| -- day to synchronize the Gregorian calendar with the astronomical year | |
| -- this extra leap day occurs in each year that is a multiple of 4, | |
| -- except for years evenly divisible by 100 but not by 400 | |
| def isLeapYear (y : ℕ) : Bool := | |
| (y % 400 == 0) || ((y % 100 != 0) && (y % 4 == 0)) | |
| -- The number of days in a month is statically defined (including) | |
| -- with/without leap years | |
| def daysInMonth (y : ℕ) (m : Month) : ℕ := | |
| match m.val with | |
| | 0 => 31 | 1 => if isLeapYear y then 29 else 28 | 2 => 31 | |
| | 3 => 30 | 4 => 31 | 5 => 30 | 6 => 31 | |
| | 7 => 31 | 8 => 30 | 9 => 31 | 10 => 30 | 11 => 31 | |
| | _ => 0 -- impossible, closes the `match` | |
| -- A date is just the number of days since some epoch (e.g., year 0, Jan 1) | |
| -- Days since the epoch **up to, but not including** the given date. | |
| def dayNumber (year : ℕ) (month : Month) (day : ℕ) : ℕ := | |
| -- days from complete years | |
| (∑ y in Finset.range year, if isLeapYear y then 366 else 365) + | |
| -- days from complete months in the current year | |
| (∑ m : Month, if m < month then daysInMonth year m else 0) + | |
| -- days before the `day`-th of this month | |
| (day - 1) | |
| -- Given a year, month, and number of days, we can calculate | |
| -- the weekday this date falls on | |
| def weekday (year : ℕ) (month : Month) (day : ℕ) : Weekday := | |
| (dayNumber year month day : Weekday) | |
| /-- | |
| `month1_offset_from_jan1 y m` is the weekday shift, modulo 7, from the 1st | |
| of January of year `y` to the 1st of `m` of the same year. | |
| It is the sum, taken in `ZMod 7`, of the lengths of all months that come | |
| **strictly before** `m`: | |
| -/ | |
| def month1_offset_from_jan1 (y : ℕ) (m : Month) : Weekday := | |
| (∑ i : Month, if i < m then (daysInMonth y i : Weekday) else 0) | |
| /-- | |
| For any given year `y`, the set of offsets (modulo 7) from January 1st to the | |
| 1st of each month spans all seven weekdays (Sunday, Monday, ...). | |
| In other words, the function `month1_offset_from_jan1 y` (which maps each month | |
| to the number of days between Jan 1 and that month's 1st, mod 7) hits every value | |
| in `ZMod 7` at least once as `m` ranges over the months. | |
| The proof proceeds by exhaustive case analysis on whether `y` is a leap year and | |
| then verifying by hand that all 7 possible offsets occur. | |
| -/ | |
| lemma monthOffset_covers_all_weekdays : | |
| (Finset.image (fun m : Month ↦ month1_offset_from_jan1 y m) Finset.univ : Finset Weekday) = Finset.univ := by { | |
| ext w | |
| constructor | |
| intro ha | |
| simp | |
| intro hb | |
| by_cases hLeap: isLeapYear y | |
| -- assuming we are in a leapyear, show that | |
| have : w ∈ | |
| (Finset.image (fun m : Month ↦ month1_offset_from_jan1 y m) Finset.univ : | |
| Finset Weekday) := by { | |
| fin_cases w | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 3;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 9;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 4;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 1;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 2;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 5;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 8;exact rfl | |
| } | |
| assumption | |
| have : w ∈ | |
| (Finset.image (fun m : Month ↦ month1_offset_from_jan1 y m) Finset.univ : | |
| Finset Weekday) := by { | |
| fin_cases w | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 9;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 4;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 7;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 1;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 5;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 8;exact rfl | |
| simp [month1_offset_from_jan1, daysInMonth, hLeap] | |
| use 3;exact rfl | |
| } | |
| assumption | |
| } | |
| -- This lemma shows that if we collect all the '1st days in a month' of a year, | |
| -- we will get the set of all weekdays | |
| lemma every_1st_is_a_weekday (y: ℕ) : | |
| (Finset.image (fun m : Month ↦ weekday y m 1) Finset.univ : | |
| Finset Weekday) = | |
| (Finset.univ : Finset Weekday) := by { | |
| ext w | |
| constructor | |
| intro ha | |
| simp | |
| intro hb | |
| -- we need to show that `w ∈ image (fun m => weekday year m 1) univ` | |
| -- or that the right side covers all weekdays | |
| have h_surj : (Finset.univ : Finset Weekday) ⊆ (Finset.image (fun m : Month ↦ weekday y m 1) Finset.univ : Finset Weekday) := by { | |
| intro w hw | |
| have h1 : (w - (weekday y 0 1)) ∈ | |
| (Finset.image (fun m : Month ↦ month1_offset_from_jan1 y m) Finset.univ : | |
| Finset Weekday) := by { | |
| -- because that image **equals** `univ` | |
| simp [monthOffset_covers_all_weekdays] | |
| } | |
| rcases Finset.mem_image.1 h1 with ⟨m, -, hm⟩ | |
| have asdf: weekday y m 1 = weekday y 0 1 + month1_offset_from_jan1 y m := by { | |
| simp [weekday, dayNumber, month1_offset_from_jan1] | |
| } | |
| simp | |
| have h2 : weekday y m 1 = w := by { | |
| rw [asdf, hm, sub_eq_add_neg] | |
| ring | |
| } | |
| use m | |
| } | |
| exact h_surj hb | |
| } | |
| -- This is almost equivalent to our main result, here | |
| -- we show that there is always a sunday the 1st, just like | |
| -- we will show there is always a friday the thirteenth | |
| theorem there_is_always_a_sunday_1st (year : ℕ) : | |
| ∃ month : Month, weekday year month 1 = 0 := by { | |
| by_contra h | |
| push_neg at h | |
| -- We have rewritten the goal. We now need to show a contradiction for | |
| -- ∀ (month : Month), weekday year month 1 ≠ 0 | |
| -- First we show sunday is in the 'out-set' of all 1st's | |
| -- we use out previous lemma to accomplish this | |
| have sunday_in_image : | |
| (0 : Weekday) ∈ (Finset.image (fun m : Month ↦ weekday year m 1) Finset.univ : | |
| Finset Weekday) := by { | |
| have : (0 : Weekday) ∈ (Finset.univ : Finset Weekday) := by simp | |
| simp [every_1st_is_a_weekday year] | |
| } | |
| -- Use to show a contradiction | |
| have ex_ha := Finset.mem_image.1 sunday_in_image | |
| cases' ex_ha with m hm | |
| exact h m hm.right | |
| } | |
| -- Friday 13th ⟺ Sunday 1st | |
| -- This is simple because if we subtract 12 days from friday the thirteenth | |
| -- we get Subday the first | |
| lemma friday_13th_iff_sunday_1st (year : ℕ) (month : Month) : | |
| weekday year month 13 = 5 ↔ weekday year month 1 = 0 := by { | |
| simp [weekday, dayNumber] | |
| have : (12 : ZMod 7) = 5 := by simp! -- simping is pimping | |
| constructor | |
| intro h | |
| rw [this] at h | |
| apply add_right_cancel h | |
| intro h | |
| rw [this] | |
| simp | |
| assumption | |
| } | |
| -- This is the main theorem, here we outline that for any year | |
| -- there exists a month such that the weekday of the 13th day | |
| -- is a friday or more canonically, every year there is a friday | |
| -- the 13th. | |
| theorem there_is_always_a_friday13th (year: ℕ) : | |
| ∃ month : Month, weekday year month 13 = 5 := by { | |
| rcases there_is_always_a_sunday_1st year with ⟨m, hSun⟩ | |
| rw [<- friday_13th_iff_sunday_1st] at hSun | |
| use m | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment