diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean
index 8ea869a52b..9b5e0f4cfd 100644
--- a/src/Lean/Elab/Tactic/Simpa.lean
+++ b/src/Lean/Elab/Tactic/Simpa.lean
@@ -24,7 +24,7 @@ namespace Lean.Elab.Tactic.Simpa
 open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter
 
 /-- Gets the value of the `linter.unnecessarySimpa` option. -/
-def getLinterUnnecessarySimpa (o : Options) : Bool :=
+def getLinterUnnecessarySimpa (o : LinterOptions) : Bool :=
   getLinterValue linter.unnecessarySimpa o
 
 deriving instance Repr for UseImplicitLambdaResult
@@ -42,7 +42,7 @@ deriving instance Repr for UseImplicitLambdaResult
     dischargeWrapper.with fun discharge? => do
       let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
           (simplifyTarget := true) (discharge? := discharge?)
-        | if getLinterUnnecessarySimpa (← getOptions) then
+        | if getLinterUnnecessarySimpa (← getLinterOptions) then
             logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
           return {}
       g.withContext do
@@ -78,7 +78,7 @@ deriving instance Repr for UseImplicitLambdaResult
             logUnassignedAndAbort (← filterOldMVars (← getMVars e) mvarCounterSaved)
             closeMainGoal `simpa (checkUnassigned := false) h
         | none =>
-          if getLinterUnnecessarySimpa (← getOptions) then
+          if getLinterUnnecessarySimpa (← getLinterOptions) then
             if let .fvar h := e then
               if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
                 logLint linter.unnecessarySimpa (← getRef)
diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean
index cda7cd6bdb..859e974ce2 100644
--- a/src/Lean/Linter.lean
+++ b/src/Lean/Linter.lean
@@ -12,3 +12,4 @@ import Lean.Linter.UnusedVariables
 import Lean.Linter.MissingDocs
 import Lean.Linter.Omit
 import Lean.Linter.List
+import Lean.Linter.Sets
diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
index c1043daa88..046f50ee67 100644
--- a/src/Lean/Linter/Basic.lean
+++ b/src/Lean/Linter/Basic.lean
@@ -5,18 +5,68 @@ Authors: Lars König
 -/
 prelude
 import Lean.Data.Options
+import Lean.MonadEnv
 import Lean.Log
 
 namespace Lean.Linter
 
+/-- Linter sets are represented as a map from linter name to set name,
+to make it easy to look up which sets to check for enabling a linter.
+-/
+def LinterSets := NameMap (Array Name)
+  deriving EmptyCollection, Inhabited
+
+/-- Insert a set into a `LinterSets` map.
+
+`entry.1` is the name of the linter set,
+`entry.2` contains the names of the set's linter options.
+-/
+def insertLinterSetEntry (map : LinterSets) (setName : Name) (options : NameSet) : LinterSets :=
+  options.fold (init := map) fun map linterName =>
+    map.insert linterName ((map.findD linterName #[]).push setName)
+
+builtin_initialize linterSetsExt : SimplePersistentEnvExtension (Name × NameSet) LinterSets ← Lean.registerSimplePersistentEnvExtension {
+  addImportedFn := mkStateFromImportedEntries (Function.uncurry <| insertLinterSetEntry ·) {}
+  addEntryFn := (Function.uncurry <| insertLinterSetEntry ·)
+  toArrayFn es := es.toArray
+}
+
+/-- The `LinterOptions` structure is used to determine whether given linters are enabled.
+
+This structure contains all the data required to do so, the `Options` set on the command line
+or by the `set_option` command, and the `LinterSets` that have been declared.
+
+A single structure holding this data is useful since we want `getLinterValue` to be a pure
+function: determinining the `LinterSets` would otherwise require a `MonadEnv` instance.
+-/
+structure LinterOptions where
+  toOptions : Options
+  linterSets : LinterSets
+
+def LinterOptions.get [KVMap.Value α] (o : LinterOptions) := o.toOptions.get (α := α)
+def LinterOptions.get? [KVMap.Value α] (o : LinterOptions) := o.toOptions.get? (α := α)
+
+def _root_.Lean.Options.toLinterOptions [Monad m] [MonadEnv m] (o : Options) : m LinterOptions := do
+  let linterSets := linterSetsExt.getState (← getEnv)
+  return { toOptions := o, linterSets }
+
+/-- Return the set of linter sets that this option is contained in. -/
+def LinterOptions.getSet (o : LinterOptions) (opt : Lean.Option α) : Array Name :=
+  o.linterSets.findD opt.name #[]
+
+def getLinterOptions [Monad m] [MonadOptions m] [MonadEnv m] : m LinterOptions := do
+  (← getOptions).toLinterOptions
+
 register_builtin_option linter.all : Bool := {
   defValue := false
   descr := "enable all linters"
 }
 
-def getLinterAll (o : Options) (defValue := linter.all.defValue) : Bool := o.get linter.all.name defValue
+def getLinterAll (o : LinterOptions) (defValue := linter.all.defValue) : Bool :=
+    o.get linter.all.name defValue
 
-def getLinterValue (opt : Lean.Option Bool) (o : Options) : Bool := o.get opt.name (getLinterAll o opt.defValue)
+def getLinterValue (opt : Lean.Option Bool) (o : LinterOptions) : Bool :=
+  o.get opt.name (getLinterAll o <| (o.getSet opt).any (o.get? · == some true) || opt.defValue)
 
 def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit :=
@@ -29,8 +79,11 @@ If `linterOption` is enabled, print a linter warning message at the position det
 Whether a linter option is enabled or not is determined by the following sequence:
 1. If it is set, then the value determines whether or not it is enabled.
 2. Otherwise, if `linter.all` is set, then its value determines whether or not the option is enabled.
-3. Otherwise, the default value determines whether or not it is enabled.
+3. Otherwise, if any of the linter sets containing the option is enabled, it is enabled.
+  (Only enabled linter sets are considered: explicitly disabling a linter set
+  will revert the linters it contains to their default behavior.)
+4. Otherwise, the default value determines whether or not it is enabled.
 -/
-def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
+def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadEnv m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do
-  if getLinterValue linterOption (← getOptions) then logLint linterOption stx msg
+  if getLinterValue linterOption (← getLinterOptions) then logLint linterOption stx msg
diff --git a/src/Lean/Linter/Builtin.lean b/src/Lean/Linter/Builtin.lean
index 9b7ca2b654..91e18e279e 100644
--- a/src/Lean/Linter/Builtin.lean
+++ b/src/Lean/Linter/Builtin.lean
@@ -14,11 +14,11 @@ register_builtin_option linter.suspiciousUnexpanderPatterns : Bool := {
   descr := "enable the 'suspicious unexpander patterns' linter"
 }
 
-def getLinterSuspiciousUnexpanderPatterns (o : Options) : Bool := getLinterValue linter.suspiciousUnexpanderPatterns o
+def getLinterSuspiciousUnexpanderPatterns (o : LinterOptions) : Bool := getLinterValue linter.suspiciousUnexpanderPatterns o
 
 def suspiciousUnexpanderPatterns : Linter where
   run cmdStx := do
-    unless getLinterSuspiciousUnexpanderPatterns (← getOptions) do
+    unless getLinterSuspiciousUnexpanderPatterns (← getLinterOptions) do
       return
 
     -- check `[app_unexpander _]` defs defined by pattern matching
diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean
index e9ac7a1ee2..2afa536fc6 100644
--- a/src/Lean/Linter/Deprecated.lean
+++ b/src/Lean/Linter/Deprecated.lean
@@ -48,7 +48,7 @@ def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name :=
   (← deprecatedAttr.getParam? env declName).newName?
 
 def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
-  if getLinterValue linter.deprecated (← getOptions) then
+  if getLinterValue linter.deprecated (← getLinterOptions) then
     let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure ()
     logWarning <| .tagged ``deprecatedAttr <|
       m!"`{.ofConstName declName true}` has been deprecated" ++ match attr.text? with
diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
index 742ad05f8b..d59fe2fe73 100644
--- a/src/Lean/Linter/MissingDocs.lean
+++ b/src/Lean/Linter/MissingDocs.lean
@@ -19,7 +19,7 @@ register_builtin_option linter.missingDocs : Bool := {
   descr := "enable the 'missing documentation' linter"
 }
 
-def getLinterMissingDocs (o : Options) : Bool := getLinterValue linter.missingDocs o
+def getLinterMissingDocs (o : LinterOptions) : Bool := getLinterValue linter.missingDocs o
 
 
 namespace MissingDocs
@@ -68,7 +68,7 @@ def getHandlers (env : Environment) : NameMap Handler := (missingDocsExt.getStat
 partial def missingDocs : Linter where
   run stx := do
     if let some h := (getHandlers (← getEnv)).find? stx.getKind then
-      h (getLinterMissingDocs (← getOptions)) stx
+      h (getLinterMissingDocs (← getLinterOptions)) stx
 
 builtin_initialize addLinter missingDocs
 
diff --git a/src/Lean/Linter/Sets.lean b/src/Lean/Linter/Sets.lean
new file mode 100644
index 0000000000..8bc3d84c6c
--- /dev/null
+++ b/src/Lean/Linter/Sets.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+prelude
+import Lean.Elab.Command
+import Lean.Linter.Basic
+
+namespace Lean.Linter
+
+/-- Add a new linter set that contains the given linters. -/
+def insertLinterSet [MonadEnv m] (setName : Name) (linterNames : NameSet) : m Unit :=
+  modifyEnv (linterSetsExt.addEntry · (setName, linterNames))
+
+/-- `registerSet` wraps `registerOption` by setting relevant values. -/
+def registerSet (setName : Name) (ref : Name := by exact decl_name%) : IO (Lean.Option Bool) := do
+  registerOption setName {
+    declName := ref
+    defValue := false
+    group := "linterSet"
+    descr := ""
+  }
+  return { name := setName, defValue := false }
+
+open Lean.Elab.Command in
+/-- Declare a new linter set by giving the set of options that will be enabled along with the set. -/
+elab doc?:(docComment)? "register_linter_set" name:ident " := " decl:ident* : command => do
+  insertLinterSet name.getId <| decl.foldl (init := ∅) fun names name => names.insert name.getId
+  let initializer ← `($[$doc?]? initialize $name : Lean.Option Bool ← Lean.Linter.registerSet $(quote name.getId))
+  withMacroExpansion (← getRef) initializer <| elabCommand initializer
+
+
+end Lean.Linter
diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index e000e70052..b5ed43cf92 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -104,29 +104,29 @@ register_builtin_option linter.unusedVariables.analyzeTactics : Bool := {
 }
 
 /-- Gets the status of `linter.unusedVariables` -/
-def getLinterUnusedVariables (o : Options) : Bool :=
+def getLinterUnusedVariables (o : LinterOptions) : Bool :=
   getLinterValue linter.unusedVariables o
 
 /-- Gets the status of `linter.unusedVariables.funArgs` -/
-def getLinterUnusedVariablesFunArgs (o : Options) : Bool :=
+def getLinterUnusedVariablesFunArgs (o : LinterOptions) : Bool :=
   o.get linter.unusedVariables.funArgs.name (getLinterUnusedVariables o)
 
 /-- Gets the status of `linter.unusedVariables.patternVars` -/
-def getLinterUnusedVariablesPatternVars (o : Options) : Bool :=
+def getLinterUnusedVariablesPatternVars (o : LinterOptions) : Bool :=
   o.get linter.unusedVariables.patternVars.name (getLinterUnusedVariables o)
 
 /-- An `IgnoreFunction` receives:
 
 * a `Syntax.ident` for the unused variable
 * a `Syntax.Stack` with the location of this piece of syntax in the command
-* The `Options` set locally to this syntax
+* The `LinterOptions` set locally to this syntax
 
 and should return `true` to indicate that the lint should be suppressed,
 or `false` to proceed with linting as usual (other `IgnoreFunction`s may still
 say it is ignored). A variable is only linted if it is unused and no
 `IgnoreFunction` returns `true` on this syntax.
 -/
-abbrev IgnoreFunction := Syntax → Syntax.Stack → Options → Bool
+abbrev IgnoreFunction := Syntax → Syntax.Stack → LinterOptions → Bool
 
 /-- Interpret an `IgnoreFunction` from the environment. -/
 unsafe def mkIgnoreFnImpl (constName : Name) : ImportM IgnoreFunction := do
@@ -381,7 +381,8 @@ structure References where
 
 /-- Collect information from the `infoTrees` into `References`.
 See `References` for more information about the return value. -/
-partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
+partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range)
+    (linterSets : LinterSets) :
     StateRefT References IO Unit := ReaderT.run (r := false) <| go infoTrees none
 where
   go infoTrees ctx? := do
@@ -422,7 +423,7 @@ where
               -- Skip declarations which are outside the command syntax range, like `variable`s
               -- (it would be confusing to lint these), or those which are macro-generated
               if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return true
-              let opts := ci.options
+              let opts : LinterOptions := { toOptions := ci.options, linterSets }
               -- we have to check for the option again here because it can be set locally
               if !getLinterUnusedVariables opts then return true
               let stx := skipDeclIdIfPresent info.stx
@@ -435,7 +436,7 @@ where
                 if let some ref := s.fvarDefs[range]? then
                   { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
                 else
-                  { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
+                  { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts := opts.toOptions, aliases := #[id] } }
             else
               -- Found a direct use, keep track of it
               modify fun s => { s with fvarUses := s.fvarUses.insert id }
@@ -471,7 +472,7 @@ private def hasSorry (stx : Syntax) : Bool :=
 /-- Reports unused variable warnings on each command. Use `linter.unusedVariables` to disable. -/
 def unusedVariables : Linter where
   run cmdStx := do
-    unless getLinterUnusedVariables (← getOptions) do
+    unless getLinterUnusedVariables (← getLinterOptions) do
       return
 
     -- NOTE: `messages` is local to the current command
@@ -488,8 +489,10 @@ def unusedVariables : Linter where
 
     let infoTrees := (← get).infoState.trees.toArray
 
+    let linterSets := linterSetsExt.getState (← getEnv)
+
     -- Run the main collection pass, resulting in `s : References`.
-    let (_, s) ← (collectReferences infoTrees cmdStxRange).run {}
+    let (_, s) ← (collectReferences infoTrees cmdStxRange linterSets).run {}
 
     -- If there are no local defs then there is nothing to do
     if s.fvarDefs.isEmpty then return
@@ -526,7 +529,8 @@ def unusedVariables : Linter where
         | continue
 
       -- If it is blacklisted by an `ignoreFn` then skip it
-      if id'.isIdent && ignoreFns.any (· declStx stack opts) then continue
+      let linterOpts ← opts.toLinterOptions
+      if id'.isIdent && ignoreFns.any (· declStx stack linterOpts) then continue
 
       -- Evaluate ignore functions again on macro expansion outputs
       if ← infoTrees.anyM fun tree => do
@@ -539,7 +543,7 @@ def unusedVariables : Linter where
               (·.getRange?.any (·.includes range))
               (fun stx => stx.isIdent && stx.getRange?.any (· == range))
           then
-            ignoreFns.any (· declStx stack opts)
+            ignoreFns.any (· declStx stack linterOpts)
           else
             false
       then
diff --git a/tests/pkg/linter_set/LinterSet.lean b/tests/pkg/linter_set/LinterSet.lean
new file mode 100644
index 0000000000..7e825c653d
--- /dev/null
+++ b/tests/pkg/linter_set/LinterSet.lean
@@ -0,0 +1,93 @@
+import LinterSet.Def
+
+open Lean Linter
+
+def fooInitially : MetaM Unit := do
+  -- linter.foo1 and linter.foo2 are declared to be false by default
+  assert! !(getLinterValue linter.foo1 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo2 (← getLinterOptions))
+  -- linter.foo_true is declared to be true by default
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval fooInitially
+
+set_option linter.set.foo true
+
+def fooSetTrue : MetaM Unit := do
+  -- All linters in the `foo` set should now be true
+  assert! (getLinterValue linter.foo1 (← getLinterOptions))
+  assert! (getLinterValue linter.foo2 (← getLinterOptions))
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval fooSetTrue
+
+section OverrideFalse
+
+set_option linter.foo2 false
+
+def overrideFalse : MetaM Unit := do
+  -- The overridden linter should now be false.
+  assert! (getLinterValue linter.foo1 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo2 (← getLinterOptions))
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval overrideFalse
+
+end OverrideFalse
+
+section AllFalse
+
+set_option linter.all false
+
+def allSetFalse : MetaM Unit := do
+  -- All linters, including those in the `foo` set, should now be false
+  assert! !(getLinterValue linter.foo1 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo2 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval allSetFalse
+
+end AllFalse
+
+set_option linter.set.foo false
+
+def fooSetFalse : MetaM Unit := do
+ -- All linters in the `foo` set should now be back to default.
+  assert! !(getLinterValue linter.foo1 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo2 (← getLinterOptions))
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval fooSetFalse
+
+section AllTrue
+
+set_option linter.all true
+
+/-- Running this code will check that all linters in the `foo` set are true.
+
+This docstring is required due to `linter.all` being true(!). -/
+def allSetTrue : MetaM Unit := do
+  -- All linters, including those in the `foo` set, should now be true
+  assert! (getLinterValue linter.foo1 (← getLinterOptions))
+  assert! (getLinterValue linter.foo2 (← getLinterOptions))
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval allSetTrue
+
+end AllTrue
+
+/-! Test setting user options from lakefile. -/
+
+open Lean
+
+def barFromLakefile : MetaM Unit := do
+  assert! (getLinterValue linter.bar (← getLinterOptions))
+
+#eval barFromLakefile
+
diff --git a/tests/pkg/linter_set/LinterSet/Def.lean b/tests/pkg/linter_set/LinterSet/Def.lean
new file mode 100644
index 0000000000..4d10d25312
--- /dev/null
+++ b/tests/pkg/linter_set/LinterSet/Def.lean
@@ -0,0 +1,12 @@
+import Lean.Linter.Sets
+
+register_option linter.foo1 : Bool := { defValue := false }
+register_option linter.foo2 : Bool := { defValue := false }
+register_option linter.foo_true : Bool := { defValue := true }
+
+register_linter_set linter.set.foo := linter.foo1 linter.foo2 linter.foo_true
+
+-- Note that we can register linter sets before their contents. Useful for `Init.lean`-style files.
+register_linter_set linter.set.bar := linter.bar
+
+register_option linter.bar : Bool := { defValue := false }
diff --git a/tests/pkg/linter_set/lakefile.toml b/tests/pkg/linter_set/lakefile.toml
new file mode 100644
index 0000000000..718552fdce
--- /dev/null
+++ b/tests/pkg/linter_set/lakefile.toml
@@ -0,0 +1,6 @@
+name = "linter_set"
+defaultTargets = ["LinterSet"]
+
+[[lean_lib]]
+name = "LinterSet"
+leanOptions = { weak.linter.set.bar = true }
diff --git a/tests/pkg/linter_set/test.sh b/tests/pkg/linter_set/test.sh
new file mode 100755
index 0000000000..b1c0671e59
--- /dev/null
+++ b/tests/pkg/linter_set/test.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf .lake/build
+lake build