diff --git a/Mathlib.lean b/Mathlib.lean
index e9deafd7b13b87..67a71201790648 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6450,6 +6450,7 @@ public import Mathlib.Tactic.Linter.MinImports
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
 public import Mathlib.Tactic.Linter.PPRoundtrip
+public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.Style
 public import Mathlib.Tactic.Linter.TextBased
 public import Mathlib.Tactic.Linter.UnusedTactic
diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean
index c9ac80b435873d..7740979dcebb5e 100644
--- a/Mathlib/Init.lean
+++ b/Mathlib/Init.lean
@@ -16,6 +16,7 @@ public import Mathlib.Tactic.Linter.FlexibleLinter
 public import Mathlib.Tactic.Linter.Lint
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
+public import Mathlib.Tactic.Linter.PrivateModule
 -- The following import contains the environment extension for the unused tactic linter.
 public import Mathlib.Tactic.Linter.UnusedTacticExtension
 public import Mathlib.Tactic.Linter.UnusedTactic
@@ -67,6 +68,7 @@ register_linter_set linter.mathlibStandardSet :=
   -- linter.checkInitImports -- disabled, not relevant downstream.
   linter.hashCommand
   linter.oldObtain
+  linter.privateModule
   linter.style.cases
   linter.style.induction
   linter.style.refine
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index 8ac71bd90b2fdf..5445911e3ecf95 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -171,6 +171,7 @@ public import Mathlib.Tactic.Linter.MinImports
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
 public import Mathlib.Tactic.Linter.PPRoundtrip
+public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.Style
 public import Mathlib.Tactic.Linter.TextBased
 public import Mathlib.Tactic.Linter.UnusedTactic
diff --git a/Mathlib/Tactic/Linter.lean b/Mathlib/Tactic/Linter.lean
index 419862edf050aa..def4f3b9441ce2 100644
--- a/Mathlib/Tactic/Linter.lean
+++ b/Mathlib/Tactic/Linter.lean
@@ -13,4 +13,5 @@ public meta import Mathlib.Tactic.Linter.DeprecatedModule
 public meta import Mathlib.Tactic.Linter.HaveLetLinter
 public meta import Mathlib.Tactic.Linter.MinImports
 public meta import Mathlib.Tactic.Linter.PPRoundtrip
+public meta import Mathlib.Tactic.Linter.PrivateModule
 public meta import Mathlib.Tactic.Linter.UpstreamableDecl
diff --git a/Mathlib/Tactic/Linter/PrivateModule.lean b/Mathlib/Tactic/Linter/PrivateModule.lean
new file mode 100644
index 00000000000000..25240e1b202593
--- /dev/null
+++ b/Mathlib/Tactic/Linter/PrivateModule.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2025 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
+module
+
+public meta import Lean.Elab.Command
+public import Lean.Linter.Basic
+public import Lean.Environment
+-- Import this linter explicitly to ensure that
+-- this file has a valid copyright header and module docstring.
+import Mathlib.Tactic.Linter.Header
+
+/-!
+# Private module linter
+
+This linter lints against nonempty modules that have only private declarations, and suggests adding
+`@[expose] public section` to the top or selectively marking declarations as `public`.
+
+## Implementation notes
+
+`env.constants.map₂` contains all locally-defined constants, and accessing this waits until all
+declarations are added. By linting (only) the `eoi` token, we can capture all constants defined in
+the file.
+
+Note that private declarations are exactly those which satisfy `isPrivateName`, whether private due
+to an explicit `private` or due to not being made `public`.
+-/
+
+meta section
+
+open Lean Elab Command Linter
+
+namespace Mathlib.Linter
+
+/-- The `privateModule` linter lints against nonempty modules that have only private declarations,
+and suggests adding `@[expose] public section` or selectively marking declarations as `public`. -/
+public register_option linter.privateModule : Bool := {
+  defValue := false
+  descr := "Enable the `privateModule` linter, which lints against nonempty modules that have only \
+    private declarations."
+}
+
+/--
+The `privateModule` linter lints against nonempty modules that have only private declarations,
+and suggests adding `@[expose] public section` to the top.
+
+This linter only acts on the end-of-input `Parser.Command.eoi` token, and ignores all other syntax.
+It logs its message at the top of the file.
+-/
+def privateModule : Linter where run stx := do
+  if stx.isOfKind ``Parser.Command.eoi then
+    unless getLinterValue linter.privateModule (← getLinterOptions) do
+      return
+    if (← getEnv).header.isModule then
+      -- Don't lint an imports-only module:
+      if !(← getEnv).constants.map₂.isEmpty then
+        -- Exit if any declaration is public:
+        for (decl, _) in (← getEnv).constants.map₂ do
+          if !isPrivateName decl then return
+        -- Lint if all names are private:
+        let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) ""
+        logLint linter.privateModule topOfFileRef
+          "The current module only contains private declarations.\n\n\
+          Consider adding `@[expose] public section` at the beginning of the module, \
+          or selectively marking declarations as `public`."
+
+initialize addLinter privateModule
+
+end Mathlib.Linter
diff --git a/MathlibTest/PrivateModuleLinter/hasOnlyPrivate.lean b/MathlibTest/PrivateModuleLinter/hasOnlyPrivate.lean
new file mode 100644
index 00000000000000..5e8c2595784ec2
--- /dev/null
+++ b/MathlibTest/PrivateModuleLinter/hasOnlyPrivate.lean
@@ -0,0 +1,30 @@
+module
+
+import Mathlib.Init
+import all Mathlib.Tactic.Linter.PrivateModule
+import Lean.Elab.Command
+
+open Lean
+
+set_option linter.mathlibStandardSet true
+
+theorem foo : True := trivial
+
+def bar : Bool := true
+
+-- Run the linter on artificial `eoi` syntax so that we can actually guard the message
+open Mathlib.Linter Parser in
+/--
+warning: The current module only contains private declarations.
+
+Consider adding `@[expose] public section` at the beginning of the module, or selectively marking declarations as `public`.
+
+Note: This linter can be disabled with `set_option linter.privateModule false`
+-/
+#guard_msgs in
+run_cmd do
+  let eoi := mkNode ``Command.eoi #[mkAtom .none ""]
+  privateModule.run eoi
+
+-- Disable so that this test is silent
+set_option linter.privateModule false
diff --git a/MathlibTest/PrivateModuleLinter/hasPublic.lean b/MathlibTest/PrivateModuleLinter/hasPublic.lean
new file mode 100644
index 00000000000000..5b09e5073241cc
--- /dev/null
+++ b/MathlibTest/PrivateModuleLinter/hasPublic.lean
@@ -0,0 +1,9 @@
+module
+
+import Mathlib.Tactic.Linter.PrivateModule
+
+set_option linter.privateModule true
+
+-- Should not fire, since `foo` is `public`.
+
+public theorem foo : True := trivial
diff --git a/MathlibTest/PrivateModuleLinter/importOnly.lean b/MathlibTest/PrivateModuleLinter/importOnly.lean
new file mode 100644
index 00000000000000..4dca009e17257c
--- /dev/null
+++ b/MathlibTest/PrivateModuleLinter/importOnly.lean
@@ -0,0 +1,8 @@
+module
+
+import Mathlib.Tactic.Linter.PrivateModule
+import Mathlib.Logic.Basic
+
+set_option linter.privateModule true
+
+/- Should not fire, since the file has no declarations. -/
diff --git a/MathlibTest/PrivateModuleLinter/nonModule.lean b/MathlibTest/PrivateModuleLinter/nonModule.lean
new file mode 100644
index 00000000000000..8653e8452e6106
--- /dev/null
+++ b/MathlibTest/PrivateModuleLinter/nonModule.lean
@@ -0,0 +1,9 @@
+import Mathlib.Tactic.Linter.PrivateModule
+
+set_option linter.privateModule true
+
+/- Should not fire because this file does not use `module`, even though it is nonempty and has only private defs. -/
+
+private theorem foo : True := trivial
+
+private def bar : Bool := true