diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index 470f266e68..2c0d1bc64d 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/src/lake/Lake/Build/Actions.lean
@@ -99,13 +99,13 @@ def mkArgs (basePath : FilePath) (args : Array String) : LogIO (Array String) :=
 
 def compileStaticLib
   (libFile : FilePath) (oFiles : Array FilePath)
-  (ar : FilePath := "ar")
+  (ar : FilePath := "ar") (thin := false)
 : LogIO Unit := do
   createParentDirs libFile
-  proc {
-    cmd := ar.toString
-    args := #["rcs", libFile.toString] ++ (← mkArgs libFile <| oFiles.map toString)
-  }
+  let args := #["rcs"]
+  let args := if thin then args.push "--thin" else args
+  let args := args.push libFile.toString ++ (← mkArgs libFile <| oFiles.map toString)
+  proc {cmd := ar.toString, args}
 
 private def getMacOSXDeploymentEnv : BaseIO (Array (String × Option String)) := do
   -- It is difficult to identify the correct minor version here, leading to linking warnings like:
diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 59116f37ac..031707bc38 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -353,11 +353,11 @@ def buildLeanO
 
 /-- Build a static library from object file jobs using the Lean toolchain's `ar`. -/
 def buildStaticLib
-  (libFile : FilePath) (oFileJobs : Array (Job FilePath))
+  (libFile : FilePath) (oFileJobs : Array (Job FilePath)) (thin :=  false)
 : SpawnM (Job FilePath) :=
   (Job.collectArray oFileJobs).mapM fun oFiles => do
     buildFileUnlessUpToDate' libFile do
-      compileStaticLib libFile oFiles (← getLeanAr)
+      compileStaticLib libFile oFiles (← getLeanAr) thin
     return libFile
 
 /--
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index 66ed3f7b2c..b084c5ff5e 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/src/lake/Lake/Build/Facets.lean
@@ -176,7 +176,14 @@ library_data leanArts : Unit
 abbrev LeanLib.staticFacet := `static
 library_data static : FilePath
 
-/-- A Lean library's static artifact (with exported symbols). -/
+/--
+A Lean library's static artifact (with exported symbols).
+
+Static libraries with explicit exports are built as thin libraries.
+Such libraries are usually used as part of the local build process of some
+shared artifact and not publicly distributed. Standard static libraries are
+much better for distribution.
+-/
 abbrev LeanLib.staticExportFacet := `static.export
 library_data static.export : FilePath
 
diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean
index ae599fd7d1..3d7c76887f 100644
--- a/src/lake/Lake/Build/Library.lean
+++ b/src/lake/Lake/Build/Library.lean
@@ -65,7 +65,12 @@ def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
   let oJobs ← mods.flatMapM fun mod =>
     mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name
   let libFile := if shouldExport then self.staticExportLibFile else self.staticLibFile
-  buildStaticLib libFile oJobs
+  /-
+  Static libraries with explicit exports are built as thin libraries.
+  The Lean build itself requires a thin static library with exported symbols
+  as part of its build process on Windows. It does not distribute this library.
+  -/
+  buildStaticLib libFile oJobs (thin := shouldExport)
 
 /-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
 def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=