diff --git a/src/Std/Time/Date/PlainDate.lean b/src/Std/Time/Date/PlainDate.lean
index 0a486e026293..eb86d52b8b6a 100644
--- a/src/Std/Time/Date/PlainDate.lean
+++ b/src/Std/Time/Date/PlainDate.lean
@@ -310,10 +310,10 @@ Determines the week of the month for the given `PlainDate`. The week of the mont
 on the day of the month and the weekday. Each week starts on Monday because the entire library is
 based on the Gregorian Calendar.
 -/
-def alignedWeekOfMonth (date : PlainDate) : Week.Ordinal.OfMonth :=
-  let weekday := date.withDaysClip 1 |>.weekday |>.toOrdinal |>.sub 1
-  let days := date.day |>.sub 1 |>.addBounds weekday
-  days |>.ediv 7 (by decide) |>.add 1
+def alignedWeekOfMonth (date : PlainDate) (firstDay : Weekday := .monday) : Week.Ordinal.OfMonth :=
+  let day1Ord := (date.withDaysClip 1).weekday.toOrdinal.val
+  let offset := (day1Ord - firstDay.toOrdinal.val + 7) % 7
+  Bounded.LE.ofNatWrapping ((date.day.val - 1 + offset) / 7 + 1) (by decide)
 
 /--
 Sets the date to the specified `desiredWeekday`. If the `desiredWeekday` is the same as the current weekday,
@@ -335,14 +335,16 @@ def withWeekday (date : PlainDate) (desiredWeekday : Weekday) : PlainDate :=
   date.addDays (Day.Offset.ofInt offset.toInt)
 
 /--
-Calculates the week of the year starting Monday for a given year.
+Calculates the week of the year for a given date, using `firstDay` as the first day of the week.
 -/
-def weekOfYear (date : PlainDate) : Week.Ordinal :=
+def weekOfYear (date : PlainDate) (firstDay : Weekday := .monday) : Week.Ordinal :=
   let y := date.year
+  let posInWeek : Bounded.LE 1 7 :=
+    .ofNatWrapping ((date.weekday.toOrdinal.val - firstDay.toOrdinal.val + 7) % 7 + 1) (by decide)
 
   let w := Bounded.LE.exact 10
     |>.addBounds date.dayOfYear
-    |>.subBounds date.weekday.toOrdinal
+    |>.subBounds posInWeek
     |>.ediv 7 (by decide)
 
   if h : w.val < 1 then
@@ -355,6 +357,24 @@ def weekOfYear (date : PlainDate) : Week.Ordinal :=
     let w := w.truncateBottom h |>.truncateTop (Int.le_trans h₁ y.weeks.property.right)
     w
 
+/--
+Returns the week-based year for the given `PlainDate`, using `firstDay` as the start of the week.
+The week-based year may differ from the calendar year for dates near the start or end of the year.
+-/
+def weekYear (date : PlainDate) (firstDay : Weekday := .monday) : Year.Offset :=
+  let y := date.year
+  let posInWeek : Bounded.LE 1 7 :=
+    .ofNatWrapping ((date.weekday.toOrdinal.val - firstDay.toOrdinal.val + 7) % 7 + 1) (by decide)
+
+  let w := Bounded.LE.exact 10
+    |>.addBounds date.dayOfYear
+    |>.subBounds posInWeek
+    |>.ediv 7 (by decide)
+
+  if w.val < 1 then y - 1
+  else if w.val > y.weeks.val then y + 1
+  else y
+
 instance : HAdd PlainDate Day.Offset PlainDate where
   hAdd := addDays
 
diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean
index 4f14a4198177..451574a1022e 100644
--- a/src/Std/Time/DateTime/PlainDateTime.lean
+++ b/src/Std/Time/DateTime/PlainDateTime.lean
@@ -489,11 +489,19 @@ def inLeapYear (date : PlainDateTime) : Bool :=
   date.year.isLeap
 
 /--
-Determines the week of the year for the given `PlainDateTime`.
+Determines the week of the year for the given `PlainDateTime`, using `firstDay` as the start of the week.
 -/
 @[inline]
-def weekOfYear (date : PlainDateTime) : Week.Ordinal :=
-  date.date.weekOfYear
+def weekOfYear (date : PlainDateTime) (firstDay : Weekday := .monday) : Week.Ordinal :=
+  date.date.weekOfYear firstDay
+
+/--
+Returns the week-based year for the given `PlainDateTime`, using `firstDay` as the start of the week.
+The week-based year may differ from the calendar year for dates near the start or end of the year.
+-/
+@[inline]
+def weekYear (date : PlainDateTime) (firstDay : Weekday := .monday) : Year.Offset :=
+  date.date.weekYear firstDay
 
 /--
 Returns the unaligned week of the month for a `PlainDateTime` (day divided by 7, plus 1).
@@ -502,13 +510,11 @@ def weekOfMonth (date : PlainDateTime) : Bounded.LE 1 5 :=
   date.date.weekOfMonth
 
 /--
-Determines the week of the month for the given `PlainDateTime`. The week of the month is calculated based
-on the day of the month and the weekday. Each week starts on Monday because the entire library is
-based on the Gregorian Calendar.
+Determines the week of the month for the given `PlainDateTime`, using `firstDay` as the start of the week.
 -/
 @[inline]
-def alignedWeekOfMonth (date : PlainDateTime) : Week.Ordinal.OfMonth :=
-  date.date.alignedWeekOfMonth
+def alignedWeekOfMonth (date : PlainDateTime) (firstDay : Weekday := .monday) : Week.Ordinal.OfMonth :=
+  date.date.alignedWeekOfMonth firstDay
 
 /--
 Transforms a tuple of a `PlainDateTime` into a `Day.Ordinal.OfYear`.
diff --git a/src/Std/Time/Format.lean b/src/Std/Time/Format.lean
index 846dce68f3a0..989575c90e2c 100644
--- a/src/Std/Time/Format.lean
+++ b/src/Std/Time/Format.lean
@@ -178,9 +178,9 @@ end TimeZone
 namespace PlainDate
 
 /--
-Formats a `PlainDate` using a specific format.
+Formats a `PlainDate` using a specific format and locale.
 -/
-def format (date : PlainDate) (format : String) : String :=
+def format (date : PlainDate) (format : String) (locale : Locale := .enUS) : String :=
   let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
@@ -189,10 +189,11 @@ def format (date : PlainDate) (format : String) : String :=
       | .G _ => some date.era
       | .y _ => some date.year
       | .u _ => some date.year
+      | .Y _ => some (date.weekYear locale.firstDayOfWeek)
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
       | .Qorq _ => some date.quarter
-      | .w _ => some date.weekOfYear
-      | .W _ => some date.alignedWeekOfMonth
+      | .w _ => some (date.weekOfYear locale.firstDayOfWeek)
+      | .W _ => some (date.alignedWeekOfMonth locale.firstDayOfWeek)
       | .MorL _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday
@@ -442,9 +443,9 @@ end ZonedDateTime
 namespace PlainDateTime
 
 /--
-Formats a `PlainDateTime` using a specific format.
+Formats a `PlainDateTime` using a specific format and locale.
 -/
-def format (date : PlainDateTime) (format : String) : String :=
+def format (date : PlainDateTime) (format : String) (locale : Locale := .enUS) : String :=
   let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
@@ -453,10 +454,11 @@ def format (date : PlainDateTime) (format : String) : String :=
       | .G _ => some date.era
       | .y _ => some date.year
       | .u _ => some date.year
+      | .Y _ => some (date.weekYear locale.firstDayOfWeek)
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
       | .Qorq _ => some date.quarter
-      | .w _ => some date.weekOfYear
-      | .W _ => some date.alignedWeekOfMonth
+      | .w _ => some (date.weekOfYear locale.firstDayOfWeek)
+      | .W _ => some (date.alignedWeekOfMonth locale.firstDayOfWeek)
       | .MorL _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday
diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean
index 4f0f6a113d84..eab48c2769ca 100644
--- a/src/Std/Time/Format/Basic.lean
+++ b/src/Std/Time/Format/Basic.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Std.Time.Zoned
+public import Std.Time.Format.Locale
 import Init.Data.String.TakeDrop
 import Init.Data.String.Search
 
@@ -24,7 +25,6 @@ open Std.Internal.Parsec Lean PlainTime PlainDate TimeZone DateTime
 
 set_option linter.all true
 
-
 /--
 `Text` represents different text formatting styles.
 -/
@@ -306,6 +306,12 @@ inductive Modifier
   -/
   | u (presentation : Year)
 
+  /--
+  `Y`: Week-based year (e.g., 2004, 04, -0001, -1).
+  The week-based year may differ from the calendar year at the start or end of the year.
+  -/
+  | Y (presentation : Year)
+
   /--
   `D`: Day of year (e.g., 189).
   -/
@@ -484,6 +490,7 @@ private def parseModifier : Parser Modifier
   := (parseText Modifier.G =<< many1Chars (pchar 'G'))
   <|> parseYear Modifier.y =<< many1Chars (pchar 'y')
   <|> parseYear Modifier.u =<< many1Chars (pchar 'u')
+  <|> parseYear Modifier.Y =<< many1Chars (pchar 'Y')
   <|> parseNumber Modifier.D =<< many1Chars (pchar 'D')
   <|> parseNumberText Modifier.MorL =<< many1Chars (pchar 'M')
   <|> parseNumberText Modifier.MorL =<< many1Chars (pchar 'L')
@@ -584,7 +591,14 @@ structure FormatConfig where
   -/
   allowLeapSeconds : Bool := false
 
-deriving Inhabited, Repr
+  /--
+  Locale configuration for formatting and parsing, including locale-specific symbols and the first
+  day of the week used for week-of-year and week-of-month calculations.
+  Default is `Locale.enUS` (English, US).
+  -/
+  locale : Locale := Locale.enUS
+
+deriving Inhabited
 
 /--
 A specification on how to format a data or parse some string.
@@ -599,7 +613,7 @@ structure GenericFormat (awareness : Awareness) where
   The format string used for parsing and formatting.
   -/
   string : FormatString
-  deriving Inhabited, Repr
+  deriving Inhabited
 
 private def parseFormatPart : Parser FormatPart
   := (.modifier <$> parseModifier)
@@ -640,119 +654,63 @@ private def rightTruncate (size : Nat)  (n : Int) (cut : Bool := false) : String
   else
     sign ++ rightPad size '0' numStr
 
-private def formatMonthLong : Month.Ordinal → String
-  | ⟨1, _⟩ => "January"
-  | ⟨2, _⟩ => "February"
-  | ⟨3, _⟩ => "March"
-  | ⟨4, _⟩ => "April"
-  | ⟨5, _⟩ => "May"
-  | ⟨6, _⟩ => "June"
-  | ⟨7, _⟩ => "July"
-  | ⟨8, _⟩ => "August"
-  | ⟨9, _⟩ => "September"
-  | ⟨10, _⟩ => "October"
-  | ⟨11, _⟩ => "November"
-  | ⟨12, _⟩ => "December"
-
-private def formatMonthShort : Month.Ordinal → String
-  | ⟨1, _⟩ => "Jan"
-  | ⟨2, _⟩ => "Feb"
-  | ⟨3, _⟩ => "Mar"
-  | ⟨4, _⟩ => "Apr"
-  | ⟨5, _⟩ => "May"
-  | ⟨6, _⟩ => "Jun"
-  | ⟨7, _⟩ => "Jul"
-  | ⟨8, _⟩ => "Aug"
-  | ⟨9, _⟩ => "Sep"
-  | ⟨10, _⟩ => "Oct"
-  | ⟨11, _⟩ => "Nov"
-  | ⟨12, _⟩ => "Dec"
-
-private def formatMonthNarrow : Month.Ordinal → String
-  | ⟨1, _⟩  => "J"
-  | ⟨2, _⟩  => "F"
-  | ⟨3, _⟩  => "M"
-  | ⟨4, _⟩  => "A"
-  | ⟨5, _⟩  => "M"
-  | ⟨6, _⟩  => "J"
-  | ⟨7, _⟩  => "J"
-  | ⟨8, _⟩  => "A"
-  | ⟨9, _⟩  => "S"
-  | ⟨10, _⟩ => "O"
-  | ⟨11, _⟩ => "N"
-  | ⟨12, _⟩ => "D"
-
-private def formatWeekdayLong : Weekday → String
-  | .sunday => "Sunday"
-  | .monday => "Monday"
-  | .tuesday => "Tuesday"
-  | .wednesday => "Wednesday"
-  | .thursday => "Thursday"
-  | .friday => "Friday"
-  | .saturday => "Saturday"
-
-private def formatWeekdayShort : Weekday → String
-  | .sunday => "Sun"
-  | .monday => "Mon"
-  | .tuesday => "Tue"
-  | .wednesday => "Wed"
-  | .thursday => "Thu"
-  | .friday => "Fri"
-  | .saturday => "Sat"
-
-private def formatWeekdayNarrow : Weekday → String
-  | .sunday => "S"
-  | .monday => "M"
-  | .tuesday => "T"
-  | .wednesday => "W"
-  | .thursday => "T"
-  | .friday => "F"
-  | .saturday => "S"
-
-private def formatEraShort : Year.Era → String
-  | .bce => "BCE"
-  | .ce  => "CE"
-
-private def formatEraLong : Year.Era → String
-  | .bce => "Before Common Era"
-  | .ce  => "Common Era"
-
-private def formatEraNarrow : Year.Era → String
-  | .bce => "B"
-  | .ce  => "C"
+private def eraIndex : Year.Era → Fin 2
+  | .bce => 0
+  | .ce => 1
+
+private def formatMonthLong (symbols : LocaleSymbols) (month : Month.Ordinal) : String :=
+  symbols.monthLong.get (month.sub 1 |>.toFin (by decide))
+
+private def formatMonthShort (symbols : LocaleSymbols) (month : Month.Ordinal) : String :=
+  symbols.monthShort.get (month.sub 1 |>.toFin (by decide))
+
+private def formatMonthNarrow (symbols : LocaleSymbols) (month : Month.Ordinal) : String :=
+  symbols.monthNarrow.get (month.sub 1 |>.toFin (by decide))
+
+private def formatWeekdayLong (symbols : LocaleSymbols) (wd : Weekday) : String :=
+  symbols.weekdayLong.get (wd.toOrdinal.sub 1 |>.toFin (by decide))
+
+private def formatWeekdayShort (symbols : LocaleSymbols) (wd : Weekday) : String :=
+  symbols.weekdayShort.get (wd.toOrdinal.sub 1 |>.toFin (by decide))
+
+private def formatWeekdayNarrow (symbols : LocaleSymbols) (wd : Weekday) : String :=
+  symbols.weekdayNarrow.get (wd.toOrdinal.sub 1 |>.toFin (by decide))
+
+private def formatEraShort (symbols : LocaleSymbols) (era : Year.Era) : String :=
+  symbols.eraShort.get (eraIndex era)
+
+private def formatEraLong (symbols : LocaleSymbols) (era : Year.Era) : String :=
+  symbols.eraLong.get (eraIndex era)
+
+private def formatEraNarrow (symbols : LocaleSymbols) (era : Year.Era) : String :=
+  symbols.eraNarrow.get (eraIndex era)
 
 private def formatQuarterNumber : Month.Quarter → String
-  |⟨1, _⟩ => "1"
-  |⟨2, _⟩ => "2"
-  |⟨3, _⟩ => "3"
-  |⟨4, _⟩ => "4"
-
-private def formatQuarterShort : Month.Quarter → String
-  | ⟨1, _⟩ => "Q1"
-  | ⟨2, _⟩ => "Q2"
-  | ⟨3, _⟩ => "Q3"
-  | ⟨4, _⟩ => "Q4"
-
-private def formatQuarterLong : Month.Quarter → String
-  | ⟨1, _⟩ => "1st quarter"
-  | ⟨2, _⟩ => "2nd quarter"
-  | ⟨3, _⟩ => "3rd quarter"
-  | ⟨4, _⟩ => "4th quarter"
-
-private def formatMarkerShort (marker : HourMarker) : String :=
+  | ⟨1, _⟩ => "1"
+  | ⟨2, _⟩ => "2"
+  | ⟨3, _⟩ => "3"
+  | ⟨4, _⟩ => "4"
+
+private def formatQuarterShort (symbols : LocaleSymbols) (q : Month.Quarter) : String :=
+  symbols.quarterShort.get (q.sub 1 |>.toFin (by decide))
+
+private def formatQuarterLong (symbols : LocaleSymbols) (q : Month.Quarter) : String :=
+  symbols.quarterLong.get (q.sub 1 |>.toFin (by decide))
+
+private def formatMarkerShort (symbols : LocaleSymbols) (marker : HourMarker) : String :=
   match marker with
-  | .am => "AM"
-  | .pm => "PM"
+  | .am => symbols.amShort
+  | .pm => symbols.pmShort
 
-private def formatMarkerLong (marker : HourMarker) : String :=
+private def formatMarkerLong (symbols : LocaleSymbols) (marker : HourMarker) : String :=
   match marker with
-  | .am => "Ante Meridiem"
-  | .pm => "Post Meridiem"
+  | .am => symbols.amLong
+  | .pm => symbols.pmLong
 
-private def formatMarkerNarrow (marker : HourMarker) : String :=
+private def formatMarkerNarrow (symbols : LocaleSymbols) (marker : HourMarker) : String :=
   match marker with
-  | .am => "A"
-  | .pm => "P"
+  | .am => symbols.amNarrow
+  | .pm => symbols.pmNarrow
 
 private def toSigned (data : Int) : String :=
   if data < 0 then toString data else "+" ++ toString data
@@ -774,6 +732,7 @@ def TypeFormat : Modifier → Type
   | .G _ => Year.Era
   | .y _ => Year.Offset
   | .u _ => Year.Offset
+  | .Y _ => Year.Offset
   | .D _ => Sigma Day.Ordinal.OfYear
   | .MorL _ => Month.Ordinal
   | .d _ => Day.Ordinal
@@ -801,18 +760,18 @@ def TypeFormat : Modifier → Type
   | .x _ => Offset
   | .Z _ => Offset
 
-private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : String :=
+private def formatWith (locale : Locale) (modifier : Modifier) (data : TypeFormat modifier) : String :=
   match modifier with
   | .G format =>
     match format with
-    | .short => formatEraShort data
-    | .full => formatEraLong data
-    | .narrow => formatEraNarrow data
+    | .short => formatEraShort locale.symbols data
+    | .full => formatEraLong locale.symbols data
+    | .narrow => formatEraNarrow locale.symbols data
   | .y format =>
     let info := data.toInt
     let info := if info ≤ 0 then -info + 1 else info
     match format with
-    | .any => pad 0 (data.toInt)
+    | .any => pad 0 info
     | .twoDigit => pad 2 (info % 100)
     | .fourDigit => pad 4 info
     | .extended n => pad n info
@@ -822,21 +781,29 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     | .twoDigit => pad 2 (data.toInt % 100)
     | .fourDigit => pad 4 data.toInt
     | .extended n => pad n data.toInt
+  | .Y format =>
+    let info := data.toInt
+    let info := if info ≤ 0 then -info + 1 else info
+    match format with
+    | .any => pad 0 info
+    | .twoDigit => pad 2 (info % 100)
+    | .fourDigit => pad 4 info
+    | .extended n => pad n info
   | .D format =>
     pad format.padding data.snd.val
   | .MorL format =>
     match format with
     | .inl format => pad format.padding data.val
-    | .inr .short => formatMonthShort data
-    | .inr .full => formatMonthLong data
-    | .inr .narrow => formatMonthNarrow data
+    | .inr .short => formatMonthShort locale.symbols data
+    | .inr .full => formatMonthLong locale.symbols data
+    | .inr .narrow => formatMonthNarrow locale.symbols data
   | .d format =>
     pad format.padding data.val
   | .Qorq format =>
     match format with
     | .inl format => pad format.padding data.val
-    | .inr .short => formatQuarterShort data
-    | .inr .full => formatQuarterLong data
+    | .inr .short => formatQuarterShort locale.symbols data
+    | .inr .full => formatQuarterLong locale.symbols data
     | .inr .narrow => formatQuarterNumber data
   | .w format =>
     pad format.padding data.val
@@ -844,22 +811,25 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
     pad format.padding data.val
   | .E format =>
     match format with
-    | .short => formatWeekdayShort data
-    | .full => formatWeekdayLong data
-    | .narrow => formatWeekdayNarrow data
+    | .short => formatWeekdayShort locale.symbols data
+    | .full => formatWeekdayLong locale.symbols data
+    | .narrow => formatWeekdayNarrow locale.symbols data
   | .eorc format =>
     match format with
-    | .inl format => pad format.padding data.toOrdinal.val
-    | .inr .short => formatWeekdayShort data
-    | .inr .full => formatWeekdayLong data
-    | .inr .narrow => formatWeekdayNarrow data
+    | .inl format =>
+      let firstOrd : Int := locale.firstDayOfWeek.toOrdinal.val
+      let dayOrd : Int := data.toOrdinal.val
+      pad format.padding ((dayOrd - firstOrd + 7) % 7 + 1)
+    | .inr .short => formatWeekdayShort locale.symbols data
+    | .inr .full => formatWeekdayLong locale.symbols data
+    | .inr .narrow => formatWeekdayNarrow locale.symbols data
   | .F format =>
     pad format.padding data.val
   | .a format =>
     match format with
-    | .short => formatMarkerShort data
-    | .full => formatMarkerLong data
-    | .narrow => formatMarkerNarrow data
+    | .short => formatMarkerShort locale.symbols data
+    | .full => formatMarkerLong locale.symbols data
+    | .narrow => formatMarkerNarrow locale.symbols data
   | .h format => pad format.padding (data.val % 12)
   | .K format => pad format.padding (data.val % 12)
   | .k format => pad format.padding data.val
@@ -920,17 +890,18 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
         then "Z"
         else  toIsoString data true (data.second.val % 60 ≠ 0) true
 
-private def dateFromModifier (date : DateTime tz) : TypeFormat modifier :=
+private def dateFromModifier (firstDay : Weekday) (date : DateTime tz) : TypeFormat modifier :=
   match modifier with
   | .G _ => date.era
   | .y _ => date.year
   | .u _ => date.year
+  | .Y _ => date.weekYear firstDay
   | .D _ => Sigma.mk _ date.dayOfYear
   | .MorL _ => date.month
   | .d _ => date.day
   | .Qorq _ => date.quarter
-  | .w _ => date.weekOfYear
-  | .W _ => date.alignedWeekOfMonth
+  | .w _ => date.weekOfYear firstDay
+  | .W _ => date.alignedWeekOfMonth firstDay
   | .E _ =>  date.weekday
   | .eorc _ => date.weekday
   | .F _ => date.weekOfMonth
@@ -953,89 +924,63 @@ private def dateFromModifier (date : DateTime tz) : TypeFormat modifier :=
   | .x _ => tz.offset
   | .Z _ => tz.offset
 
-private def parseMonthLong : Parser Month.Ordinal
-   := pstring "January" *> pure ⟨1, by decide⟩
-  <|> pstring "February" *> pure ⟨2, by decide⟩
-  <|> pstring "March" *> pure ⟨3, by decide⟩
-  <|> pstring "April" *> pure ⟨4, by decide⟩
-  <|> pstring "May" *> pure ⟨5, by decide⟩
-  <|> pstring "June" *> pure ⟨6, by decide⟩
-  <|> pstring "July" *> pure ⟨7, by decide⟩
-  <|> pstring "August" *> pure ⟨8, by decide⟩
-  <|> pstring "September" *> pure ⟨9, by decide⟩
-  <|> pstring "October" *> pure ⟨10, by decide⟩
-  <|> pstring "November" *> pure ⟨11, by decide⟩
-  <|> pstring "December" *> pure ⟨12, by decide⟩
+private def parseFromSymbols {α : Type} (pairs : Array (String × α)) : Parser α :=
+  pairs.foldl (fun acc (s, v) => acc <|> pstring s *> pure v) (fail "no match")
+
+private def monthPairs (arr : Vector String 12) : Array (String × Month.Ordinal) :=
+  arr.mapFinIdx (fun idx val n => (val, Bounded.LE.ofFin ⟨idx, n⟩ |>.add 1)) |>.toArray
+
+private def weekdayOfIndex : Nat → Weekday
+  | 0 => .sunday
+  | 1 => .monday
+  | 2 => .tuesday
+  | 3 => .wednesday
+  | 4 => .thursday
+  | 5 => .friday
+  | _ => .saturday
+
+private def weekdayPairs (arr : Vector String 7) : Array (String × Weekday) :=
+  arr.mapFinIdx (fun idx val n => (val, .ofOrdinal <| Bounded.LE.ofFin ⟨idx, n⟩ |>.add 1)) |>.toArray
+
+private def eraOfIndex : Nat → Year.Era
+  | 0 => .bce
+  | _ => .ce
+
+private def eraPairs (arr : Vector String 2) : Array (String × Year.Era) :=
+  arr.mapFinIdx (fun idx val _ => (val, eraOfIndex idx)) |>.toArray
+
+private def quarterPairs (arr : Vector String 4) : Array (String × Month.Quarter) :=
+  arr.mapFinIdx (fun idx val n => (val, Bounded.LE.ofFin ⟨idx, n⟩ |>.add 1)) |>.toArray
+
+private def parseMonthLong (symbols : LocaleSymbols) : Parser Month.Ordinal :=
+  parseFromSymbols (monthPairs symbols.monthLong)
 
 /--
-Parses a short value of a `Month.Ordinal`
+Parses a short month name using the given locale symbols and returns the corresponding `Month.Ordinal`.
 -/
-def parseMonthShort : Parser Month.Ordinal
-   := pstring "Jan" *> pure ⟨1, by decide⟩
-  <|> pstring "Feb" *> pure ⟨2, by decide⟩
-  <|> pstring "Mar" *> pure ⟨3, by decide⟩
-  <|> pstring "Apr" *> pure ⟨4, by decide⟩
-  <|> pstring "May" *> pure ⟨5, by decide⟩
-  <|> pstring "Jun" *> pure ⟨6, by decide⟩
-  <|> pstring "Jul" *> pure ⟨7, by decide⟩
-  <|> pstring "Aug" *> pure ⟨8, by decide⟩
-  <|> pstring "Sep" *> pure ⟨9, by decide⟩
-  <|> pstring "Oct" *> pure ⟨10, by decide⟩
-  <|> pstring "Nov" *> pure ⟨11, by decide⟩
-  <|> pstring "Dec" *> pure ⟨12, by decide⟩
-
-private def parseMonthNarrow : Parser Month.Ordinal
-   := pstring "J" *> pure ⟨1, by decide⟩
-  <|> pstring "F" *> pure ⟨2, by decide⟩
-  <|> pstring "M" *> pure ⟨3, by decide⟩
-  <|> pstring "A" *> pure ⟨4, by decide⟩
-  <|> pstring "M" *> pure ⟨5, by decide⟩
-  <|> pstring "J" *> pure ⟨6, by decide⟩
-  <|> pstring "J" *> pure ⟨7, by decide⟩
-  <|> pstring "A" *> pure ⟨8, by decide⟩
-  <|> pstring "S" *> pure ⟨9, by decide⟩
-  <|> pstring "O" *> pure ⟨10, by decide⟩
-  <|> pstring "N" *> pure ⟨11, by decide⟩
-  <|> pstring "D" *> pure ⟨12, by decide⟩
-
-private def parseWeekdayLong : Parser Weekday
-   := pstring "Sunday" *> pure Weekday.sunday
-  <|> pstring "Monday" *> pure Weekday.monday
-  <|> pstring "Tuesday" *> pure Weekday.tuesday
-  <|> pstring "Wednesday" *> pure Weekday.wednesday
-  <|> pstring "Thursday" *> pure Weekday.thursday
-  <|> pstring "Friday" *> pure Weekday.friday
-  <|> pstring "Saturday" *> pure Weekday.saturday
-
-private def parseWeekdayShort : Parser Weekday
-   := pstring "Sun" *> pure Weekday.sunday
-  <|> pstring "Mon" *> pure Weekday.monday
-  <|> pstring "Tue" *> pure Weekday.tuesday
-  <|> pstring "Wed" *> pure Weekday.wednesday
-  <|> pstring "Thu" *> pure Weekday.thursday
-  <|> pstring "Fri" *> pure Weekday.friday
-  <|> pstring "Sat" *> pure Weekday.saturday
-
-private def parseWeekdayNarrow : Parser Weekday
-   := pstring "S" *> pure Weekday.sunday
-  <|> pstring "M" *> pure Weekday.monday
-  <|> pstring "T" *> pure Weekday.tuesday
-  <|> pstring "W" *> pure Weekday.wednesday
-  <|> pstring "T" *> pure Weekday.thursday
-  <|> pstring "F" *> pure Weekday.friday
-  <|> pstring "S" *> pure Weekday.saturday
-
-private def parseEraShort : Parser Year.Era
-   := pstring "BCE" *> pure Year.Era.bce
-  <|> pstring "CE" *> pure Year.Era.ce
-
-private def parseEraLong : Parser Year.Era
-   := pstring "Before Common Era" *> pure Year.Era.bce
-  <|> pstring "Common Era" *> pure Year.Era.ce
-
-private def parseEraNarrow : Parser Year.Era
-   := pstring "B" *> pure Year.Era.bce
-  <|> pstring "C" *> pure Year.Era.ce
+def parseMonthShort (symbols : LocaleSymbols) : Parser Month.Ordinal :=
+  parseFromSymbols (monthPairs symbols.monthShort)
+
+private def parseMonthNarrow (symbols : LocaleSymbols) : Parser Month.Ordinal :=
+  parseFromSymbols (monthPairs symbols.monthNarrow)
+
+private def parseWeekdayLong (symbols : LocaleSymbols) : Parser Weekday :=
+  parseFromSymbols (weekdayPairs symbols.weekdayLong)
+
+private def parseWeekdayShort (symbols : LocaleSymbols) : Parser Weekday :=
+  parseFromSymbols (weekdayPairs symbols.weekdayShort)
+
+private def parseWeekdayNarrow (symbols : LocaleSymbols) : Parser Weekday :=
+  parseFromSymbols (weekdayPairs symbols.weekdayNarrow)
+
+private def parseEraShort (symbols : LocaleSymbols) : Parser Year.Era :=
+  parseFromSymbols (eraPairs symbols.eraShort)
+
+private def parseEraLong (symbols : LocaleSymbols) : Parser Year.Era :=
+  parseFromSymbols (eraPairs symbols.eraLong)
+
+private def parseEraNarrow (symbols : LocaleSymbols) : Parser Year.Era :=
+  parseFromSymbols (eraPairs symbols.eraNarrow)
 
 private def parseQuarterNumber : Parser Month.Quarter
    := pstring "1" *> pure ⟨1, by decide⟩
@@ -1043,29 +988,20 @@ private def parseQuarterNumber : Parser Month.Quarter
   <|> pstring "3" *> pure ⟨3, by decide⟩
   <|> pstring "4" *> pure ⟨4, by decide⟩
 
-private def parseQuarterLong : Parser Month.Quarter
-   := pstring "1st quarter" *> pure ⟨1, by decide⟩
-  <|> pstring "2nd quarter" *> pure ⟨2, by decide⟩
-  <|> pstring "3rd quarter" *> pure ⟨3, by decide⟩
-  <|> pstring "4th quarter" *> pure ⟨4, by decide⟩
+private def parseQuarterLong (symbols : LocaleSymbols) : Parser Month.Quarter :=
+  parseFromSymbols (quarterPairs symbols.quarterLong)
 
-private def parseQuarterShort : Parser Month.Quarter
-   := pstring "Q1" *> pure ⟨1, by decide⟩
-  <|> pstring "Q2" *> pure ⟨2, by decide⟩
-  <|> pstring "Q3" *> pure ⟨3, by decide⟩
-  <|> pstring "Q4" *> pure ⟨4, by decide⟩
+private def parseQuarterShort (symbols : LocaleSymbols) : Parser Month.Quarter :=
+  parseFromSymbols (quarterPairs symbols.quarterShort)
 
-private def parseMarkerShort : Parser HourMarker
-   := pstring "AM" *> pure HourMarker.am
-  <|> pstring "PM" *> pure HourMarker.pm
+private def parseMarkerShort (symbols : LocaleSymbols) : Parser HourMarker :=
+  (pstring symbols.amShort *> pure .am) <|> (pstring symbols.pmShort *> pure .pm)
 
-private def parseMarkerLong : Parser HourMarker
-   := pstring "Ante Meridiem" *> pure HourMarker.am
-  <|> pstring "Post Meridiem" *> pure HourMarker.pm
+private def parseMarkerLong (symbols : LocaleSymbols) : Parser HourMarker :=
+  (pstring symbols.amLong *> pure .am) <|> (pstring symbols.pmLong *> pure .pm)
 
-private def parseMarkerNarrow : Parser HourMarker
-   := pstring "A" *> pure HourMarker.am
-  <|> pstring "P" *> pure HourMarker.pm
+private def parseMarkerNarrow (symbols : LocaleSymbols) : Parser HourMarker :=
+  (pstring symbols.amNarrow *> pure .am) <|> (pstring symbols.pmNarrow *> pure .pm)
 
 private def exactly (parse : Parser α) (size : Nat) : Parser (Array α) :=
   let rec go (acc : Array α) (count : Nat) : Parser (Array α) :=
@@ -1158,9 +1094,9 @@ private def parseOffset (withMinutes : Reason) (withSeconds : Reason) (withColon
 private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (TypeFormat mod)
   | .G format =>
     match format with
-    | .short => parseEraShort
-    | .full => parseEraLong
-    | .narrow => parseEraNarrow
+    | .short => parseEraShort config.locale.symbols
+    | .full => parseEraLong config.locale.symbols
+    | .narrow => parseEraNarrow config.locale.symbols
   | .y format =>
     match format with
     | .any => Int.ofNat <$> parseAtLeastNum 1
@@ -1173,39 +1109,50 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ
     | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2
     | .fourDigit => parseSigned <| parseNum 4
     | .extended n => parseSigned <| parseNum n
+  | .Y format =>
+    match format with
+    | .any => parseSigned <| parseAtLeastNum 1
+    | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2
+    | .fourDigit => parseSigned <| parseNum 4
+    | .extended n => parseSigned <| parseNum n
   | .D format => Sigma.mk true <$> parseNatToBounded (parseFlexibleNum format.padding)
   | .MorL format =>
     match format with
     | .inl format => parseNatToBounded (parseFlexibleNum format.padding)
-    | .inr .short => parseMonthShort
-    | .inr .full => parseMonthLong
-    | .inr .narrow => parseMonthNarrow
+    | .inr .short => parseMonthShort config.locale.symbols
+    | .inr .full => parseMonthLong config.locale.symbols
+    | .inr .narrow => parseMonthNarrow config.locale.symbols
   | .d format => parseNatToBounded (parseFlexibleNum format.padding)
   | .Qorq format =>
     match format with
     | .inl format => parseNatToBounded (parseFlexibleNum format.padding)
-    | .inr .short => parseQuarterShort
-    | .inr .full => parseQuarterLong
+    | .inr .short => parseQuarterShort config.locale.symbols
+    | .inr .full => parseQuarterLong config.locale.symbols
     | .inr .narrow => parseQuarterNumber
   | .w format => parseNatToBounded (parseFlexibleNum format.padding)
   | .W format => parseNatToBounded (parseFlexibleNum format.padding)
   | .E format =>
     match format with
-    | .short => parseWeekdayShort
-    | .full => parseWeekdayLong
-    | .narrow => parseWeekdayNarrow
+    | .short => parseWeekdayShort config.locale.symbols
+    | .full => parseWeekdayLong config.locale.symbols
+    | .narrow => parseWeekdayNarrow config.locale.symbols
   | .eorc format =>
     match format with
-    | .inl format => Weekday.ofOrdinal <$> parseNatToBounded (parseFlexibleNum format.padding)
-    | .inr .short => parseWeekdayShort
-    | .inr .full => parseWeekdayLong
-    | .inr .narrow => parseWeekdayNarrow
+    | .inl format => do
+      let n ← parseFlexibleNum format.padding
+      if ¬ (1 ≤ n ∧ n ≤ 7) then fail "need a natural number in the interval of 1 to 7"
+      let firstOrd : Int := config.locale.firstDayOfWeek.toOrdinal.val
+      let absOrd : Int := ((n : Int) - 1 + firstOrd - 1) % 7 + 1
+      return Weekday.ofOrdinal (Bounded.LE.ofNatWrapping absOrd (by decide))
+    | .inr .short => parseWeekdayShort config.locale.symbols
+    | .inr .full => parseWeekdayLong config.locale.symbols
+    | .inr .narrow => parseWeekdayNarrow config.locale.symbols
   | .F format => parseNatToBounded (parseFlexibleNum format.padding)
   | .a format =>
     match format with
-    | .short => parseMarkerShort
-    | .full => parseMarkerLong
-    | .narrow => parseMarkerNarrow
+    | .short => parseMarkerShort config.locale.symbols
+    | .full => parseMarkerLong config.locale.symbols
+    | .narrow => parseMarkerNarrow config.locale.symbols
   | .h format => parseNatToBounded (parseFlexibleNum format.padding)
   | .K format => parseNatToBounded (parseFlexibleNum format.padding)
   | .k format => parseNatToBounded (parseFlexibleNum format.padding)
@@ -1266,9 +1213,9 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ
       (skipString "Z" *> pure Offset.zero)
       <|> (parseOffset .yes .optional true)
 
-private def formatPartWithDate (date : DateTime tz) (part : FormatPart) : String :=
+private def formatPartWithDate (locale : Locale) (date : DateTime tz) (part : FormatPart) : String :=
   match part with
-  | .modifier mod => formatWith mod (dateFromModifier date)
+  | .modifier mod => formatWith locale mod (dateFromModifier locale.firstDayOfWeek date)
   | .string s => s
 
 set_option linter.missingDocs false in  -- TODO
@@ -1284,6 +1231,7 @@ private structure DateBuilder where
   G : Option Year.Era := none
   y : Option Year.Offset := none
   u : Option Year.Offset := none
+  Y : Option Year.Offset := none
   D : Option (Sigma Day.Ordinal.OfYear) := none
   MorL : Option Month.Ordinal := none
   d : Option Day.Ordinal := none
@@ -1319,6 +1267,7 @@ private def insert (date : DateBuilder) (modifier : Modifier) (data : TypeFormat
   | .G _ => { date with G := some data }
   | .y _ => { date with y := some data }
   | .u _ => { date with u := some data }
+  | .Y _ => { date with Y := some data }
   | .D _ => { date with D := some data }
   | .MorL _ => { date with MorL := some data }
   | .d _ => { date with d := some data }
@@ -1368,6 +1317,7 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type :=
   let year
     := builder.u
     <|> ((convertYearAndEra · era) <$> builder.y)
+    <|> builder.Y
     |>.getD 0
 
   let hour : Option (Bounded.LE 0 23) :=
@@ -1433,10 +1383,11 @@ def spec! (input : String) (config : FormatConfig := {}) : GenericFormat tz :=
 Formats a `DateTime` value into a string using the given `GenericFormat`.
 -/
 def format (format : GenericFormat aw) (date : DateTime tz) : String :=
+  let locale := format.config.locale
   let mapper (part : FormatPart) :=
     match aw with
-    | .any => formatPartWithDate date part
-    | .only tz => formatPartWithDate (date.convertTimeZone tz) part
+    | .any => formatPartWithDate locale date part
+    | .only tz => formatPartWithDate locale (date.convertTimeZone tz) part
 
   format.string.map mapper
   |> String.join
@@ -1499,8 +1450,9 @@ def parseBuilder! [Inhabited α] (format : GenericFormat aw)  (builder : FormatT
 Formats the date using the format into a String, using a `getInfo` function to get the information needed to build the `String`.
 -/
 def formatGeneric (format : GenericFormat aw) (getInfo : (typ : Modifier) → Option (TypeFormat typ)) : Option String :=
+  let locale := format.config.locale
   let rec go (data : String) : (format : FormatString) → Option String
-    | .modifier x :: xs => do go (data ++ formatWith x (← getInfo x)) xs
+    | .modifier x :: xs => do go (data ++ formatWith locale x (← getInfo x)) xs
     | .string x :: xs => go (data ++ x) xs
     | [] => some data
   go "" format.string
@@ -1509,8 +1461,9 @@ def formatGeneric (format : GenericFormat aw) (getInfo : (typ : Modifier) → Op
 Constructs a `FormatType` function to format a date into a string using a `GenericFormat`.
 -/
 def formatBuilder (format : GenericFormat aw) : FormatType String format.string :=
+  let locale := format.config.locale
   let rec go (data : String) : (format : FormatString) → FormatType String format
-    | .modifier x :: xs => fun res => go (data ++ formatWith x res) xs
+    | .modifier x :: xs => fun res => go (data ++ formatWith locale x res) xs
     | .string x :: xs => go (data ++ x) xs
     | [] => data
   go "" format.string
diff --git a/src/Std/Time/Format/Locale.lean b/src/Std/Time/Format/Locale.lean
new file mode 100644
index 000000000000..bcef0a478431
--- /dev/null
+++ b/src/Std/Time/Format/Locale.lean
@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Init.Data.Vector.Extract
+public import Std.Time.Date.Unit.Weekday
+
+public section
+
+namespace Std
+namespace Time
+
+set_option linter.all true
+
+/--
+`LocaleSymbols` contains locale-specific strings needed for date/time formatting and parsing.
+
+Arrays are 0-indexed: `monthLong[0]` = January, `weekdayLong[0]` = Sunday, `eraShort[0]` = BCE.
+-/
+structure LocaleSymbols where
+
+  /--
+  Full month names (12 elements, index 0 = January).
+  -/
+  monthLong : Vector String 12
+
+  /--
+  Abbreviated month names (12 elements, index 0 = Jan).
+  -/
+  monthShort : Vector String 12
+
+  /--
+  Narrow month names (12 elements, index 0 = J).
+  -/
+  monthNarrow : Vector String 12
+
+  /--
+  Full weekday names (7 elements, index 0 = Monday).
+  -/
+  weekdayLong : Vector String 7
+
+  /--
+  Abbreviated weekday names (7 elements, index 0 = Mon).
+  -/
+  weekdayShort : Vector String 7
+
+  /--
+  Narrow weekday names (7 elements, index 0 = M).
+  -/
+  weekdayNarrow : Vector String 7
+
+  /--
+  Short era names (2 elements: index 0 = BCE, index 1 = CE).
+  -/
+  eraShort : Vector String 2
+
+  /--
+  Full era names (2 elements: index 0 = Before Common Era, index 1 = Common Era).
+  -/
+  eraLong : Vector String 2
+
+  /--
+  Narrow era names (2 elements: index 0 = B, index 1 = C).
+  -/
+  eraNarrow : Vector String 2
+
+  /--
+  Short quarter names (4 elements, index 0 = Q1).
+  -/
+  quarterShort : Vector String 4
+
+  /--
+  Full quarter names (4 elements, index 0 = 1st quarter).
+  -/
+  quarterLong : Vector String 4
+
+  /--
+  Narrow quarter names (4 elements, index 0 = 1).
+  -/
+  quarterNarrow : Vector String 4
+
+  /--
+  Short AM marker.
+  -/
+  amShort : String
+
+  /--
+  Short PM marker.
+  -/
+  pmShort : String
+
+  /--
+  Full AM marker.
+  -/
+  amLong : String
+
+  /--
+  Full PM marker.
+  -/
+  pmLong : String
+
+  /--
+  Narrow AM marker.
+  -/
+  amNarrow : String
+
+  /--
+  Narrow PM marker.
+  -/
+  pmNarrow : String
+
+namespace LocaleSymbols
+
+/--
+English (US) locale symbols.
+-/
+def enUS : LocaleSymbols where
+  monthLong := Vector.mk #["January", "February", "March", "April", "May", "June", "July", "August", "September", "October", "November", "December"] (by decide)
+  monthShort := Vector.mk #["Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"] (by decide)
+  monthNarrow := Vector.mk #["J", "F", "M", "A", "M", "J", "J", "A", "S", "O", "N", "D"] (by decide)
+  weekdayLong := Vector.mk #["Monday", "Tuesday", "Wednesday", "Thursday", "Friday", "Saturday", "Sunday"] (by decide)
+  weekdayShort := Vector.mk #["Mon", "Tue", "Wed", "Thu", "Fri", "Sat", "Sun"] (by decide)
+  weekdayNarrow := Vector.mk #["M", "T", "W", "T", "F", "S", "S"] (by decide)
+  eraShort := Vector.mk #["BCE", "CE"] (by decide)
+  eraLong := Vector.mk #["Before Common Era", "Common Era"] (by decide)
+  eraNarrow := Vector.mk #["B", "C"] (by decide)
+  quarterShort := Vector.mk #["Q1", "Q2", "Q3", "Q4"] (by decide)
+  quarterLong := Vector.mk #["1st quarter", "2nd quarter", "3rd quarter", "4th quarter"] (by decide)
+  quarterNarrow := Vector.mk #["1", "2", "3", "4"] (by decide)
+  amShort := "AM"
+  pmShort := "PM"
+  amLong := "Ante Meridiem"
+  pmLong := "Post Meridiem"
+  amNarrow := "A"
+  pmNarrow := "P"
+
+end LocaleSymbols
+
+/--
+`Locale` contains locale-specific configuration for date/time formatting and parsing,
+combining calendar conventions (e.g. first day of week) with locale symbols.
+-/
+structure Locale where
+
+  /--
+  The first day of the week for this locale (e.g., `Weekday.sunday` for US, `Weekday.monday` for ISO 8601).
+  -/
+  firstDayOfWeek : Weekday := .sunday
+
+  /--
+  Locale-specific symbols used for formatting and parsing text fields.
+  -/
+  symbols : LocaleSymbols := LocaleSymbols.enUS
+
+namespace Locale
+
+/--
+English (US) locale.
+-/
+def enUS : Locale where
+  firstDayOfWeek := .sunday
+  symbols := LocaleSymbols.enUS
+
+end Locale
+
+end Time
+end Std
diff --git a/src/Std/Time/Notation.lean b/src/Std/Time/Notation.lean
index 9d02a01a9d92..e568cebdcd5e 100644
--- a/src/Std/Time/Notation.lean
+++ b/src/Std/Time/Notation.lean
@@ -59,6 +59,7 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .G p => do `(Std.Time.Modifier.G $(← convertText p))
   | .y p => do `(Std.Time.Modifier.y $(← convertYear p))
   | .u p => do `(Std.Time.Modifier.u $(← convertYear p))
+  | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p))
   | .D p => do `(Std.Time.Modifier.D $(← convertNumber p))
   | .MorL p =>
     match p with
diff --git a/src/Std/Time/Notation/Spec.lean b/src/Std/Time/Notation/Spec.lean
index d3efdd9a45b2..014093bdd604 100644
--- a/src/Std/Time/Notation/Spec.lean
+++ b/src/Std/Time/Notation/Spec.lean
@@ -57,6 +57,7 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .G p => do `(Std.Time.Modifier.G $(← convertText p))
   | .y p => do `(Std.Time.Modifier.y $(← convertYear p))
   | .u p => do `(Std.Time.Modifier.u $(← convertYear p))
+  | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p))
   | .D p => do `(Std.Time.Modifier.D $(← convertNumber p))
   | .MorL p =>
     match p with
diff --git a/src/Std/Time/Zoned/DateTime.lean b/src/Std/Time/Zoned/DateTime.lean
index 8049652e0143..4229d2c63146 100644
--- a/src/Std/Time/Zoned/DateTime.lean
+++ b/src/Std/Time/Zoned/DateTime.lean
@@ -432,11 +432,19 @@ def dayOfYear (date : DateTime tz) : Day.Ordinal.OfYear date.year.isLeap :=
   ValidDate.dayOfYear ⟨⟨date.month, date.day⟩, date.date.get.date.valid⟩
 
 /--
-Determines the week of the year for the given `DateTime`.
+Determines the week of the year for the given `DateTime`, using `firstDay` as the start of the week.
 -/
 @[inline]
-def weekOfYear (date : DateTime tz) : Week.Ordinal :=
-  date.date.get.weekOfYear
+def weekOfYear (date : DateTime tz) (firstDay : Weekday := .monday) : Week.Ordinal :=
+  date.date.get.weekOfYear firstDay
+
+/--
+Returns the week-based year for the given `DateTime`, using `firstDay` as the start of the week.
+The week-based year may differ from the calendar year for dates near the start or end of the year.
+-/
+@[inline]
+def weekYear (date : DateTime tz) (firstDay : Weekday := .monday) : Year.Offset :=
+  date.date.get.weekYear firstDay
 
 /--
 Returns the unaligned week of the month for a `DateTime` (day divided by 7, plus 1).
@@ -445,13 +453,11 @@ def weekOfMonth (date : DateTime tz) : Bounded.LE 1 5 :=
   date.date.get.weekOfMonth
 
 /--
-Determines the week of the month for the given `DateTime`. The week of the month is calculated based
-on the day of the month and the weekday. Each week starts on Monday because the entire library is
-based on the Gregorian Calendar.
+Determines the week of the month for the given `DateTime`, using `firstDay` as the start of the week.
 -/
 @[inline]
-def alignedWeekOfMonth (date : DateTime tz) : Week.Ordinal.OfMonth :=
-  date.date.get.alignedWeekOfMonth
+def alignedWeekOfMonth (date : DateTime tz) (firstDay : Weekday := .monday) : Week.Ordinal.OfMonth :=
+  date.date.get.alignedWeekOfMonth firstDay
 
 /--
 Determines the quarter of the year for the given `DateTime`.
diff --git a/src/Std/Time/Zoned/ZonedDateTime.lean b/src/Std/Time/Zoned/ZonedDateTime.lean
index 062b0a50de25..34a939d8e6db 100644
--- a/src/Std/Time/Zoned/ZonedDateTime.lean
+++ b/src/Std/Time/Zoned/ZonedDateTime.lean
@@ -224,11 +224,19 @@ def dayOfYear (date : ZonedDateTime) : Day.Ordinal.OfYear date.year.isLeap :=
   ValidDate.dayOfYear ⟨(date.month, date.day), date.date.get.date.valid⟩
 
 /--
-Determines the week of the year for the given `ZonedDateTime`.
+Determines the week of the year for the given `ZonedDateTime`, using `firstDay` as the start of the week.
 -/
 @[inline]
-def weekOfYear (date : ZonedDateTime) : Week.Ordinal :=
-  date.date.get.weekOfYear
+def weekOfYear (date : ZonedDateTime) (firstDay : Weekday := .monday) : Week.Ordinal :=
+  date.date.get.weekOfYear firstDay
+
+/--
+Returns the week-based year for the given `ZonedDateTime`, using `firstDay` as the start of the week.
+The week-based year may differ from the calendar year for dates near the start or end of the year.
+-/
+@[inline]
+def weekYear (date : ZonedDateTime) (firstDay : Weekday := .monday) : Year.Offset :=
+  date.date.get.weekYear firstDay
 
 /--
 Returns the unaligned week of the month for a `ZonedDateTime` (day divided by 7, plus 1).
@@ -237,13 +245,11 @@ def weekOfMonth (date : ZonedDateTime) : Internal.Bounded.LE 1 5 :=
   date.date.get.weekOfMonth
 
 /--
-Determines the week of the month for the given `ZonedDateTime`. The week of the month is calculated based
-on the day of the month and the weekday. Each week starts on Monday because the entire library is
-based on the Gregorian Calendar.
+Determines the week of the month for the given `ZonedDateTime`, using `firstDay` as the start of the week.
 -/
 @[inline]
-def alignedWeekOfMonth (date : ZonedDateTime) : Week.Ordinal.OfMonth :=
-  date.date.get.alignedWeekOfMonth
+def alignedWeekOfMonth (date : ZonedDateTime) (firstDay : Weekday := .monday) : Week.Ordinal.OfMonth :=
+  date.date.get.alignedWeekOfMonth firstDay
 
 /--
 Determines the quarter of the year for the given `ZonedDateTime`.
diff --git a/tests/elab/timeFormats.lean b/tests/elab/timeFormats.lean
index baa6571f87d5..82037c99d8e2 100644
--- a/tests/elab/timeFormats.lean
+++ b/tests/elab/timeFormats.lean
@@ -339,13 +339,13 @@ info: "3 03 3rd quarter 3"
 #eval zoned₄.format "Q QQ QQQQ QQQQQ"
 
 /--
-info: "28 28 028 0028"
+info: "29 29 029 0029"
 -/
 #guard_msgs in
 #eval zoned₄.format "w ww www wwww"
 
 /--
-info: "2 02 002 0002"
+info: "3 03 003 0003"
 -/
 #guard_msgs in
 #eval zoned₄.format "W WW WWW WWWW"
@@ -357,7 +357,7 @@ info: "Sun Sun Sun Sunday S"
 #eval zoned₄.format "E EE EEE EEEE EEEEE"
 
 /--
-info: "7 07 Sun Sunday S"
+info: "1 01 Sun Sunday S"
 -/
 #guard_msgs in
 #eval zoned₄.format "e ee eee eeee eeeee"
@@ -536,13 +536,13 @@ info: "3 03 3rd quarter 3"
 #eval datetime₄.format "Q QQ QQQQ QQQQQ"
 
 /--
-info: "28 28 028 0028"
+info: "29 29 029 0029"
 -/
 #guard_msgs in
 #eval datetime₄.format "w ww www wwww"
 
 /--
-info: "2 02 002 0002"
+info: "3 03 003 0003"
 -/
 #guard_msgs in
 #eval datetime₄.format "W WW WWW WWWW"
@@ -554,7 +554,7 @@ info: "Sun Sun Sun Sunday S"
 #eval datetime₄.format "E EE EEE EEEE EEEEE"
 
 /--
-info: "7 07 Sun Sunday S"
+info: "1 01 Sun Sunday S"
 -/
 #guard_msgs in
 #eval datetime₄.format "e ee eee eeee eeeee"
@@ -752,13 +752,13 @@ info: "3 03 3rd quarter 3"
 #eval date₄.format "Q QQ QQQQ QQQQQ"
 
 /--
-info: "28 28 028 0028"
+info: "29 29 029 0029"
 -/
 #guard_msgs in
 #eval date₄.format "w ww www wwww"
 
 /--
-info: "2 02 002 0002"
+info: "3 03 003 0003"
 -/
 #guard_msgs in
 #eval date₄.format "W WW WWW WWWW"
@@ -770,7 +770,7 @@ info: "Sun Sun Sun Sunday S"
 #eval date₄.format "E EE EEE EEEE EEEEE"
 
 /--
-info: "7 07 Sun Sunday S"
+info: "1 01 Sun Sunday S"
 -/
 #guard_msgs in
 #eval date₄.format "e ee eee eeee eeeee"