diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7704d8f..77f32a0 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -40,5 +40,8 @@ jobs:
       - name: Check quoted module and declaration paths
         run: lake build test_module_paths && lake env .lake/build/bin/test_module_paths
 
+      - name: Check workspace dependency selection
+        run: lake build test_dependencies && lake env .lake/build/bin/test_dependencies
+
       - name: Check Python test harnesses
         run: python3 -m py_compile tests/scripts/*.py
diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean
index 0f706dd..34d8e57 100644
--- a/LeanEvalGenerator/Contract.lean
+++ b/LeanEvalGenerator/Contract.lean
@@ -57,6 +57,12 @@ structure GenerateRequest where
   contextRoot : String
   leanToolchain : String
   mathlib : DependencyPin
+  /-- Optional non-mathlib git requires, in the order a workspace should
+  require them. Each is emitted, before Mathlib, into the workspace of every
+  problem that imports one of its modules (the rule is
+  `LeanEvalGenerator.Core.workspaceRequires`). Omitting the field means no
+  extra requires, which is how every earlier version 1 request behaves. -/
+  dependencies : Option (Array DependencyPin) := none
   templates : TemplateInputs
   problems : Array ProblemInput
   deriving FromJson
@@ -75,6 +81,18 @@ private def validateRequest (request : GenerateRequest) : IO Unit := do
     throw <| IO.userError "The dependency pin must be named `mathlib`."
   if request.mathlib.git.isEmpty || request.mathlib.rev.isEmpty then
     throw <| IO.userError "The mathlib git and rev pins must be non-empty."
+  let mut dependencyNames : Array String := #[]
+  for dep in request.dependencies.getD #[] do
+    if dep.name.isEmpty then
+      throw <| IO.userError "Dependency names must be non-empty."
+    if dep.name == "mathlib" then
+      throw <| IO.userError
+        "`dependencies` must not contain `mathlib`; it is pinned by the `mathlib` field."
+    if dependencyNames.contains dep.name then
+      throw <| IO.userError s!"Duplicate dependency `{dep.name}`."
+    if dep.git.isEmpty || dep.rev.isEmpty then
+      throw <| IO.userError s!"Dependency `{dep.name}` git and rev pins must be non-empty."
+    dependencyNames := dependencyNames.push dep.name
   let mut problemIds : Array String := #[]
   for problem in request.problems do
     if problemIds.contains problem.id then
@@ -123,8 +141,10 @@ private def extracted (hole : ResolvedHole) : LeanEvalGenerator.Core.ExtractedTh
 }
 
 private def validateProblem (root : System.FilePath) (problem : ProblemInput) : IO Unit := do
-  if problem.id.isEmpty then
-    throw <| IO.userError "Problem id must be non-empty."
+  unless LeanEvalGenerator.Core.isValidProblemId problem.id do
+    throw <| IO.userError
+      s!"Problem id {problem.id.quote} is invalid. Use only letters, digits, '_' or '-', \
+        starting with a letter or digit."
   if problem.title.isEmpty then
     throw <| IO.userError s!"Problem `{problem.id}` title must be non-empty."
   if problem.moduleName.isEmpty then
@@ -190,16 +210,18 @@ ordered and byte-stable, including complete file contents and SHA-256 digests. -
 def render (request : GenerateRequest) : IO String := do
   validateRequest request
   let root : System.FilePath := request.contextRoot
-  let mathlib : LeanEvalGenerator.Core.DependencySpec := {
-    name := request.mathlib.name
-    git := request.mathlib.git
-    rev := request.mathlib.rev
+  let spec (pin : DependencyPin) : LeanEvalGenerator.Core.DependencySpec :=
+    { name := pin.name, git := pin.git, rev := pin.rev }
+  let deps : LeanEvalGenerator.Core.RootDependencies := {
+    mathlib := spec request.mathlib
+    extras := (request.dependencies.getD #[]).map
+      (LeanEvalGenerator.Core.RootRequire.ofSpec ∘ spec)
   }
   let mut files : Array LeanEvalGenerator.Core.OJson := #[]
   for problem in request.problems do
     validateProblem root problem
     let rendered ← LeanEvalGenerator.Core.renderWorkspace root (metadata problem)
-      (problem.resolvedHoles.map extracted) request.leanToolchain mathlib
+      (problem.resolvedHoles.map extracted) request.leanToolchain deps
       request.templates.workspaceTest
     for (path, content) in rendered do
       files := files.push <| fileJson problem.id path content (← sha256 content)
@@ -217,10 +239,14 @@ private def ensureKnownFields (label : String) (allowed : Array String)
 
 private def validateJsonShape (value : Json) : Except String Unit := do
   ensureKnownFields "request" #[
-    "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "templates", "problems"
+    "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "dependencies", "templates",
+    "problems"
   ] value
   let mathlib ← value.getObjVal? "mathlib"
   ensureKnownFields "mathlib" #["name", "git", "rev"] mathlib
+  if let .ok deps := value.getObjVal? "dependencies" then
+    for dep in ← deps.getArr? do
+      ensureKnownFields "dependency" #["name", "git", "rev"] dep
   let templates ← value.getObjVal? "templates"
   ensureKnownFields "templates" #["workspaceTest"] templates
   let problems ← (← value.getObjVal? "problems").getArr?
diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean
index 686e9a8..9013df1 100644
--- a/LeanEvalGenerator/Core/Generate.lean
+++ b/LeanEvalGenerator/Core/Generate.lean
@@ -42,7 +42,7 @@ def ignoredPathNames : Array String := #[".lake", "build", ".cache", "lake-manif
 def loadWorkspaceTestTemplate (root : System.FilePath) : IO String :=
   IO.FS.readFile (root / "templates" / "WorkspaceTest.lean")
 
-/-! ## Mathlib dependency -/
+/-! ## Root dependencies -/
 
 structure DependencySpec where
   name : String
@@ -50,22 +50,70 @@ structure DependencySpec where
   rev : String
   deriving Inhabited
 
-private structure RawRequire where
+/-- A `[[require]]` from the root lakefile, kept as read. Non-mathlib requires
+are only validated when some problem selects them (see `workspaceRequires`), so
+tooling requires the generator never emits may use any Lake require syntax. -/
+structure RootRequire where
   name : String
   git : Option String := none
   rev : Option String := none
+  /-- Fields present in the root require that a generated `[[require]]` would
+  not reproduce, such as `subDir`, `scope`, `version`, `path`, `options`, or a
+  table-valued `git`. -/
+  unsupportedFields : Array String := #[]
   deriving Inhabited
 
-private instance : DecodeToml RawRequire where
-  decode v := do
-    let t ← v.decodeTable
-    let name : String ← t.decode `name
-    let git? : Option String ← t.decode? `git
-    let rev? : Option String ← t.decode? `rev
-    return { name := name, git := git?, rev := rev? }
+def RootRequire.ofSpec (spec : DependencySpec) : RootRequire :=
+  { name := spec.name, git := some spec.git, rev := some spec.rev }
+
+private def nonEmptyTrimmed? (value? : Option String) : Option String :=
+  value?.bind fun v => let v := v.trim; if v.isEmpty then none else some v
+
+/-- The `[[require]]` to emit for a selected root require, or an explanation of
+why a standalone workspace cannot reproduce it. -/
+def RootRequire.toSpec (r : RootRequire) : Except String DependencySpec := do
+  unless r.unsupportedFields.isEmpty do
+    throw s!"root require '{r.name}' uses fields a generated workspace does not \
+      reproduce: {", ".intercalate r.unsupportedFields.toList}. Only `name`, `git` \
+      and `rev` are supported."
+  let some git := nonEmptyTrimmed? r.git
+    | throw s!"root require '{r.name}' is not a git require with a non-empty `git` URL"
+  let some rev := nonEmptyTrimmed? r.rev
+    | throw s!"root require '{r.name}' does not pin a non-empty `rev`"
+  return { name := r.name, git, rev }
+
+private def rootRequireOfTable (t : Table) : Except String RootRequire := do
+  let name ← match t.find? `name with
+    | some (.string _ n) => pure n
+    | _ => throw "a [[require]] entry is missing a string `name` field"
+  let mut git : Option String := none
+  let mut rev : Option String := none
+  let mut unsupported : Array String := #[]
+  for (key, value) in t.items do
+    match key.toString, value with
+    | "name", _ => pure ()
+    | "git", .string _ g => git := some g
+    | "git", _ => unsupported := unsupported.push "table-valued `git`"
+    | "rev", .string _ r => rev := some r
+    | "rev", _ => unsupported := unsupported.push "non-string `rev`"
+    | other, _ => unsupported := unsupported.push s!"`{other}`"
+  return { name, git, rev, unsupportedFields := unsupported }
+
+/-- The dependencies a generated workspace may require, read from the root
+lakefile: the mandatory `mathlib` pin, plus every other root `[[require]]` in
+root lakefile order. An extra require is only emitted into a workspace whose
+problem imports one of its modules; see `workspaceRequires`. -/
+structure RootDependencies where
+  mathlib : DependencySpec
+  extras : Array RootRequire := #[]
+  deriving Inhabited
 
-def loadRootMathlibDependency (root : System.FilePath) : IO DependencySpec := do
-  let path := root / "lakefile.toml"
+/-- A bare `mathlib` pin is a complete dependency set with no extras, so
+callers holding only a `DependencySpec` keep working unchanged. -/
+instance : Coe DependencySpec RootDependencies where
+  coe mathlib := { mathlib }
+
+private def loadRootRequires (path : System.FilePath) : IO (Array RootRequire) := do
   let contents ← IO.FS.readFile path
   let inputCtx := mkInputContext contents path.toString
   let table ←
@@ -73,38 +121,60 @@ def loadRootMathlibDependency (root : System.FilePath) : IO DependencySpec := do
     | .ok table => pure table
     | .error err => throw <| IO.userError (← Lake.mkMessageLogString err)
   let decoded :
-      EStateM.Result Unit (Array DecodeError) (Array RawRequire) :=
-    (Lake.Toml.Table.decode (α := Array RawRequire) table `require).run #[]
-  let requires ←
-    match decoded with
+      EStateM.Result Unit (Array DecodeError) (Array Table) :=
+    (Lake.Toml.Table.decode (α := Array Table) table `require).run #[]
+  let tables ← match decoded with
     | .ok arr errors =>
         if errors.isEmpty then pure arr
         else throw <| IO.userError (decodeErrorsToString errors)
     | .error _ errors =>
         throw <| IO.userError (decodeErrorsToString errors)
-  let mathlib := requires.filter fun r => r.name == "mathlib"
+  tables.mapM fun t => match rootRequireOfTable t with
+    | .ok r => pure r
+    | .error e => throw <| IO.userError s!"{path}: {e}"
+
+private def requiredField (path : System.FilePath) (depName field : String)
+    (value? : Option String) : IO String := do
+  match nonEmptyTrimmed? value? with
+  | some v => pure v
+  | none =>
+      throw <| IO.userError
+        s!"{depName} dependency in {path} is missing a non-empty '{field}' field"
+
+private def loadRootDependenciesCore (root : System.FilePath) (strictMathlib : Bool) :
+    IO RootDependencies := do
+  let path := root / "lakefile.toml"
+  let rootRequires ← loadRootRequires path
+  let mathlib := rootRequires.filter fun r => r.name == "mathlib"
   if mathlib.isEmpty then
     throw <| IO.userError s!"Could not find a mathlib dependency in {path}"
   if mathlib.size > 1 then
     throw <| IO.userError s!"Found multiple mathlib dependencies in {path}"
   let entry := mathlib[0]!
-  let git ← match entry.git with
-    | some g =>
-        let g := g.trim
-        if g.isEmpty then
-          throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'git' field"
-        else pure g
-    | none =>
-        throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'git' field"
-  let rev ← match entry.rev with
-    | some r =>
-        let r := r.trim
-        if r.isEmpty then
-          throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'rev' field"
-        else pure r
-    | none =>
-        throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'rev' field"
-  return { name := "mathlib", git := git, rev := rev }
+  if strictMathlib && !entry.unsupportedFields.isEmpty then
+    throw <| IO.userError
+      s!"mathlib dependency in {path} uses fields a generated workspace does not \
+        reproduce: {", ".intercalate entry.unsupportedFields.toList}. Only `name`, \
+        `git` and `rev` are supported."
+  let git ← requiredField path "mathlib" "git" entry.git
+  let rev ← requiredField path "mathlib" "rev" entry.rev
+  return {
+    mathlib := { name := "mathlib", git := git, rev := rev }
+    extras := rootRequires.filter (·.name != "mathlib")
+  }
+
+/-- Read the root `lakefile.toml` for workspace generation: the single
+`mathlib` require, which must be a plain git require with non-empty `git` and
+`rev` and no other fields, and every other require as written. Other requires
+are not validated here; a problem that selects one fails if it cannot be
+reproduced (see `RootRequire.toSpec`). -/
+def loadRootDependencies (root : System.FilePath) : IO RootDependencies :=
+  loadRootDependenciesCore root (strictMathlib := true)
+
+/-- The root `mathlib` pin. Unlike `loadRootDependencies`, this ignores
+fields beyond `name`, `git` and `rev`, as it always has. -/
+def loadRootMathlibDependency (root : System.FilePath) : IO DependencySpec :=
+  return (← loadRootDependenciesCore root (strictMathlib := false)).mathlib
 
 /-! ## ExtractedTheorem (subprocess result) -/
 
@@ -1251,6 +1321,15 @@ private partial def collectWorkspaceImports (root : System.FilePath) (moduleName
       unless (← out.get).contains imported do
         out.modify (·.push imported)
 
+/-- The external modules a generated workspace imports, in the order
+`problemImportHeader` emits them. -/
+def problemWorkspaceImports (root : System.FilePath) (moduleName : String) :
+    IO (Array String) := do
+  let visited ← IO.mkRef ({} : Std.HashSet String)
+  let out ← IO.mkRef (#[] : Array String)
+  collectWorkspaceImports root moduleName visited out
+  out.get
+
 /-- The `import` header a generated workspace needs to reproduce the trusted
 module's elaboration context.
 
@@ -1270,12 +1349,42 @@ Known limitation: flattening several repo-local modules into one
 so an inlined module can see a name that only a later one introduced. Avoiding
 that would mean emitting one workspace module per source module. -/
 def problemImportHeader (root : System.FilePath) (moduleName : String) : IO String := do
-  let visited ← IO.mkRef ({} : Std.HashSet String)
-  let out ← IO.mkRef (#[] : Array String)
-  collectWorkspaceImports root moduleName visited out
-  let imports ← out.get
+  let imports ← problemWorkspaceImports root moduleName
   return String.join (imports.toList.map fun m => s!"import {m}\n")
 
+/-- The `[[require]]` entries for a workspace whose modules import `imports`
+(as returned by `problemWorkspaceImports`, so repo-local imports have already
+been followed): each extra root require whose `name` equals the first
+component of some imported module, in root lakefile order, followed by
+`mathlib`. For example `import TauCeti.Foo.Bar` selects the require named
+`TauCeti`. Tooling requires in the root lakefile are never selected, because
+no problem imports them. Fails if a selected require cannot be reproduced.
+
+Known limitation: a package whose library root differs from its package name
+(say package `foo-bar` providing modules `FooBar.*`) is not matched. Its
+workspace then lacks the require, and the workspace build fails loudly on the
+missing import rather than silently changing the statement.
+
+Mathlib must come last. When two requires share a transitive dependency
+(batteries, aesop, Qq, ...), Lake resolves it from the later require, so
+putting an extra package after Mathlib would make `lake update` pick up that
+package's (typically older) pins instead of Mathlib's. -/
+def workspaceRequires (deps : RootDependencies) (imports : Array String) :
+    Except String (Array DependencySpec) := do
+  let roots : Std.HashSet String := imports.foldl (init := {}) fun acc m =>
+    match (splitNameComponents m)[0]? with
+    | some r => acc.insert r
+    | none => acc
+  let selected ← (deps.extras.filter fun r => roots.contains r.name).mapM (·.toSpec)
+  return selected.push deps.mathlib
+
+/-- `workspaceRequires` for the workspace generated from `moduleName`. -/
+def problemWorkspaceRequires (root : System.FilePath) (deps : RootDependencies)
+    (problemId moduleName : String) : IO (Array DependencySpec) := do
+  match workspaceRequires deps (← problemWorkspaceImports root moduleName) with
+  | .ok specs => pure specs
+  | .error e => throw <| IO.userError s!"Problem '{problemId}': {e}"
+
 /-! ## ILean metadata -/
 
 /-- A declaration's source range from the `.ilean`, as
@@ -2892,21 +3001,44 @@ private def renderReadmeLines (entry : EvalProblemMetadata)
       ]
   return lines ++ body
 
-private def lakefileToml (problemId : String) (mathlibDep : DependencySpec)
+/-- A TOML basic string literal for `s`: backslash, double quote and control
+characters are escaped; anything else (in particular every ordinary package
+name, URL and revision) is emitted verbatim between double quotes. -/
+def tomlBasicString (s : String) : String := Id.run do
+  let mut out := "\""
+  for c in s.toList do
+    out := match c with
+      | '\\' => out ++ "\\\\"
+      | '"' => out ++ "\\\""
+      | '\n' => out ++ "\\n"
+      | '\t' => out ++ "\\t"
+      | '\r' => out ++ "\\r"
+      | c =>
+          if c.toNat < 0x20 || c.toNat == 0x7f then
+            let hex := String.mk (Nat.toDigits 16 c.toNat)
+            out ++ "\\u" ++ String.mk (List.replicate (4 - hex.length) '0') ++ hex
+          else out.push c
+  return out.push '"'
+
+/-- Render a workspace `lakefile.toml`. `workspaceDeps` is emitted in the given
+order; see `workspaceRequires` for why Mathlib must be last. -/
+def lakefileToml (problemId : String) (workspaceDeps : Array DependencySpec)
     (withChallengeDeps : Bool) : String :=
   let challengeDepsLib :=
     if withChallengeDeps then
       "[[lean_lib]]\nname = \"ChallengeDeps\"\n\n"
     else ""
-  s!"name = \"{problemId}\"\n" ++
+  let requireBlocks := String.join <| workspaceDeps.toList.map fun dep =>
+    "[[require]]\n" ++
+    s!"name = {tomlBasicString dep.name}\n" ++
+    s!"git = {tomlBasicString dep.git}\n" ++
+    s!"rev = {tomlBasicString dep.rev}\n\n"
+  s!"name = {tomlBasicString problemId}\n" ++
   "testDriver = \"workspace_test\"\n" ++
   "defaultTargets = [\"Challenge\", \"Solution\", \"Submission\"]\n\n" ++
   "[leanOptions]\n" ++
   "autoImplicit = false\n\n" ++
-  "[[require]]\n" ++
-  s!"name = \"{mathlibDep.name}\"\n" ++
-  s!"git = \"{mathlibDep.git}\"\n" ++
-  s!"rev = \"{mathlibDep.rev}\"\n\n" ++
+  requireBlocks ++
   challengeDepsLib ++
   "[[lean_lib]]\nname = \"Challenge\"\n\n" ++
   "[[lean_lib]]\nname = \"Solution\"\n\n" ++
@@ -2917,7 +3049,7 @@ private def lakefileToml (problemId : String) (mathlibDep : DependencySpec)
 
 private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProblemMetadata)
     (extracteds : Array ExtractedTheorem) (toolchain : String)
-    (mathlibDep : DependencySpec) (workspaceTest : String) :
+    (deps : RootDependencies) (workspaceTest : String) :
     IO (Array (String × String)) := do
   let sourcePath := moduleSourcePath root entry.moduleName
   if !(← sourcePath.pathExists) then
@@ -3132,6 +3264,7 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl
     if hasChallengeDeps then removeDuplicatedReducibilityAttributes helperStripped depsHelpers
     else helperStripped
   let moduleImports ← problemImportHeader root entry.moduleName
+  let workspaceDeps ← problemWorkspaceRequires root deps entry.id entry.moduleName
   let baseImport := if hasChallengeDeps then "import ChallengeDeps\n\n" else moduleImports ++ "\n"
   let challengeBodyStripped := stripProblemMarkers helperStripped localImports
   let challengeBody :=
@@ -3179,7 +3312,8 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl
   let mut files : Array (String × String) := #[
     ("README.md", readme),
     ("lean-toolchain", toolchain'),
-    ("lakefile.toml", lakefileToml entry.id mathlibDep (withChallengeDeps := hasChallengeDeps)),
+    ("lakefile.toml",
+      lakefileToml entry.id workspaceDeps (withChallengeDeps := hasChallengeDeps)),
     ("Challenge.lean", challenge),
     ("Solution.lean", solutionBody),
     ("Submission.lean", submissionBody),
@@ -3194,7 +3328,7 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl
 /-! ## Single-hole rendering -/
 
 private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProblemMetadata)
-    (extracted : ExtractedTheorem) (toolchain : String) (mathlibDep : DependencySpec)
+    (extracted : ExtractedTheorem) (toolchain : String) (deps : RootDependencies)
     (workspaceTest : String) : IO (Array (String × String)) := do
   let sourcePath := moduleSourcePath root entry.moduleName
   let sourceText ← IO.FS.readFile sourcePath
@@ -3208,6 +3342,7 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb
   let challengeDeps? ← renderChallengeDeps root entry extracted localImports
   let hasChallengeDeps := challengeDeps?.isSome
   let moduleImports ← problemImportHeader root entry.moduleName
+  let workspaceDeps ← problemWorkspaceRequires root deps entry.id entry.moduleName
   let challengeImport :=
     if hasChallengeDeps then "import ChallengeDeps\n\n" else moduleImports ++ "\n"
   let solutionImports :=
@@ -3283,7 +3418,8 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb
   let mut files : Array (String × String) := #[
     ("README.md", readme),
     ("lean-toolchain", toolchain'),
-    ("lakefile.toml", lakefileToml entry.id mathlibDep (withChallengeDeps := hasChallengeDeps)),
+    ("lakefile.toml",
+      lakefileToml entry.id workspaceDeps (withChallengeDeps := hasChallengeDeps)),
     ("Challenge.lean", challengeFile),
     ("Solution.lean", solutionFile),
     ("Submission.lean", submissionFile),
@@ -3298,15 +3434,15 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb
 /-- Render every file in a generated workspace. Mirrors `render_workspace`. -/
 def renderWorkspace (root : System.FilePath) (entry : EvalProblemMetadata)
     (extracteds : Array ExtractedTheorem) (toolchain : String)
-    (mathlibDep : DependencySpec) (workspaceTest : String) :
+    (deps : RootDependencies) (workspaceTest : String) :
     IO (Array (String × String)) := do
   let isMultiHole :=
     extracteds.size != 1 || extracteds[0]!.kind != "theorem"
   let baseFiles ←
     if isMultiHole then
-      renderWorkspaceMultiHole root entry extracteds toolchain mathlibDep workspaceTest
+      renderWorkspaceMultiHole root entry extracteds toolchain deps workspaceTest
     else
-      renderWorkspaceSingleHole root entry extracteds[0]! toolchain mathlibDep workspaceTest
+      renderWorkspaceSingleHole root entry extracteds[0]! toolchain deps workspaceTest
   let holesJson ← buildHolesMetadata root entry extracteds
   return baseFiles.push ("holes.json", holesJson)
 
@@ -3512,7 +3648,7 @@ def generate (root : System.FilePath) (selectedProblemId : Option String) (check
         pure problems
   validateHoleShape root selectedProblems
   let toolchain ← IO.FS.readFile (root / "lean-toolchain")
-  let mathlibDep ← loadRootMathlibDependency root
+  let deps ← loadRootDependencies root
   buildExtractor root selectedProblems
   let workspaceTest ← loadWorkspaceTestTemplate root
   let mut mismatches : Array String := #[]
@@ -3521,7 +3657,7 @@ def generate (root : System.FilePath) (selectedProblemId : Option String) (check
     for hole in entry.holes do
       let e ← extractOne root entry hole
       extracteds := extracteds.push e
-    let files ← renderWorkspace root entry extracteds toolchain mathlibDep workspaceTest
+    let files ← renderWorkspace root entry extracteds toolchain deps workspaceTest
     let problemDir := root / "generated" / entry.id
     let relDisplay := s!"generated/{entry.id}"
     if check then
diff --git a/LeanEvalGenerator/Core/Manifest.lean b/LeanEvalGenerator/Core/Manifest.lean
index 3690afc..9e412b8 100644
--- a/LeanEvalGenerator/Core/Manifest.lean
+++ b/LeanEvalGenerator/Core/Manifest.lean
@@ -17,7 +17,7 @@ private def isAsciiAlnum (c : Char) : Bool :=
   c.isAlpha || c.isDigit
 
 /-- Mirrors the Python `ID_PATTERN = re.compile(r"^[A-Za-z0-9][A-Za-z0-9_-]*$")`. -/
-private def isValidProblemId (s : String) : Bool :=
+def isValidProblemId (s : String) : Bool :=
   !s.isEmpty
     && isAsciiAlnum s.front
     && s.all (fun c => isAsciiAlnum c || c == '_' || c == '-')
diff --git a/README.md b/README.md
index 70103ab..e098f44 100644
--- a/README.md
+++ b/README.md
@@ -27,3 +27,31 @@ The consumer owns hole resolution. A consumer resolves declarations under its
 pinned target environment, then passes the resulting ranges and dependency
 data to this renderer. Consumer-specific fixtures and source trees do not
 belong in this foundation package.
+
+## Workspace dependencies
+
+Every generated `lakefile.toml` requires Mathlib at the pinned revision. A
+problem may also import modules from another package. The library API reads
+the candidate packages from the consumer's root `lakefile.toml`
+(`loadRootDependencies`); a CLI request lists them in the optional
+`dependencies` array of `{name, git, rev}` pins, and omitting that array means
+Mathlib only. A candidate is required by a workspace exactly when its `name`
+equals the first component of a module the problem imports, after following
+repo-local imports: `import TauCeti.Foo.Bar` selects the package named
+`TauCeti`. Tooling packages are therefore never required, because no problem
+imports them. Selected packages are emitted in root order before Mathlib,
+which stays last so that Lake resolves shared transitive dependencies from
+Mathlib's pins.
+
+A selected root require must be a plain git require with a non-empty `git` and
+`rev`; `subDir`, `scope`, `options`, a table-valued `git` or any other field is
+an error, since the workspace would not reproduce it. Unselected requires are
+not checked. A package whose library root differs from its package name is not
+matched; the generated workspace then fails to build on the missing import
+rather than silently changing the statement.
+
+The emitted requires are pruned to what the problem imports, but their
+transitive dependencies are not pinned in the workspace lakefile. A consumer
+that builds a generated workspace should install the root `lake-manifest.json`
+into it (as lean-eval's CI does) rather than running `lake update`, so that
+every package resolves to the same revision as in the root workspace.
diff --git a/Tests/Dependencies.lean b/Tests/Dependencies.lean
new file mode 100644
index 0000000..c820e26
--- /dev/null
+++ b/Tests/Dependencies.lean
@@ -0,0 +1,152 @@
+import LeanEvalGenerator.Core.Generate
+
+open LeanEvalGenerator.Core
+
+private def expectEq (label actual expected : String) : IO Unit := do
+  unless actual == expected do
+    throw <| IO.userError
+      s!"{label} mismatch\nexpected:\n{repr expected}\nactual:\n{repr actual}"
+
+private def mathlibRev := "d13f23b723b8a846827a245b89c10fc7d3f11612"
+private def tauCetiRev := "7cfdfef3ac31cce91302b926ac2f49525eed6fbc"
+
+private def rootLakefile : String :=
+  "name = \"fixture\"\n\n" ++
+  "[[require]]\nname = \"mathlib\"\n" ++
+  "git = \"https://github.com/leanprover-community/mathlib4.git\"\n" ++
+  s!"rev = \"{mathlibRev}\"\n\n" ++
+  "[[require]]\nname = \"TauCeti\"\n" ++
+  "git = \"https://github.com/TauCetiProject/TauCeti\"\n" ++
+  s!"rev = \"{tauCetiRev}\"\n\n" ++
+  -- Tooling requires that no problem imports may use any Lake syntax: none of
+  -- these is validated unless a problem selects it.
+  "[[require]]\nname = \"Cli\"\n" ++
+  "git = \"https://github.com/leanprover/lean4-cli\"\n\n" ++
+  "[[require]]\nname = \"LocalTool\"\npath = \"tools/local\"\n\n" ++
+  "[[require]]\nname = \"Reservoir\"\nscope = \"someone\"\nversion = \"1.0\"\n\n" ++
+  "[[require]]\nname = \"SubDirPkg\"\ngit = \"https://example.com/x\"\n" ++
+  "rev = \"abc\"\nsubDir = \"pkg\"\n\n" ++
+  "[[require]]\nname = \"TableGit\"\ngit = { url = \"https://example.com/y\" }\n" ++
+  "rev = \"abc\"\n"
+
+private def requireBlock (name git rev : String) : String :=
+  s!"[[require]]\nname = \"{name}\"\ngit = \"{git}\"\nrev = \"{rev}\"\n\n"
+
+private def mathlibBlock : String :=
+  requireBlock "mathlib" "https://github.com/leanprover-community/mathlib4.git" mathlibRev
+
+/-- The lakefile every Mathlib-only workspace had before extra requires
+existed, spelled out literally so any drift in its bytes is caught. -/
+private def mathlibOnlyLakefile (problemId : String) : String :=
+  s!"name = \"{problemId}\"\n" ++
+  "testDriver = \"workspace_test\"\n" ++
+  "defaultTargets = [\"Challenge\", \"Solution\", \"Submission\"]\n\n" ++
+  "[leanOptions]\nautoImplicit = false\n\n" ++
+  mathlibBlock ++
+  "[[lean_lib]]\nname = \"Challenge\"\n\n" ++
+  "[[lean_lib]]\nname = \"Solution\"\n\n" ++
+  "[[lean_lib]]\nname = \"Submission\"\n\n" ++
+  "[[lean_exe]]\nname = \"workspace_test\"\nroot = \"WorkspaceTest\"\n"
+
+private def writeModule (root : System.FilePath) (moduleName source : String) : IO Unit := do
+  let path := moduleSourcePath root moduleName
+  if let some dir := path.parent then IO.FS.createDirAll dir
+  IO.FS.writeFile path source
+
+private def requiresFor (root : System.FilePath) (deps : RootDependencies)
+    (moduleName : String) : IO (Array DependencySpec) :=
+  problemWorkspaceRequires root deps moduleName moduleName
+
+/-- Selecting the require that `import {package}.X` pulls in must fail with a
+message containing `expected`. -/
+private def expectSelectionError (deps : RootDependencies) (package expected : String) :
+    IO Unit := do
+  match workspaceRequires deps #[s!"{package}.X", "Mathlib.Logic.Basic"] with
+  | .ok specs =>
+      throw <| IO.userError
+        s!"selecting {package} should fail, but gave {specs.map (·.name)}"
+  | .error e =>
+      unless (e.splitOn expected).length > 1 do
+        throw <| IO.userError s!"selecting {package}: error {e.quote} lacks {expected.quote}"
+
+private def names (specs : Array DependencySpec) : String :=
+  toString (specs.map (·.name))
+
+def main : IO Unit := do
+  let root ← IO.FS.createTempDir
+  try
+    IO.FS.writeFile (root / "lakefile.toml") rootLakefile
+    -- The TauCeti import is reached only through a repo-local helper module.
+    writeModule root "LeanEval.Cfsg"
+      "import Mathlib.GroupTheory.Perm.Basic\nimport LeanEval.CfsgHelper\n"
+    writeModule root "LeanEval.CfsgHelper"
+      "import TauCeti.GroupTheory.SpecificGroups.CFSG.Classification\n"
+    writeModule root "LeanEval.Plain" "import Mathlib.Data.Nat.Basic\n"
+
+    let deps ← loadRootDependencies root
+    expectEq "mathlib pin" deps.mathlib.rev mathlibRev
+    expectEq "extra requires" (toString (deps.extras.map (·.name)))
+      "#[TauCeti, Cli, LocalTool, Reservoir, SubDirPkg, TableGit]"
+    expectEq "legacy loader" (← loadRootMathlibDependency root).rev mathlibRev
+
+    -- Unreproducible requires only fail once a problem selects them.
+    expectSelectionError deps "Cli" "does not pin a non-empty `rev`"
+    expectSelectionError deps "LocalTool" "`path`"
+    expectSelectionError deps "Reservoir" "`scope`, `version`"
+    expectSelectionError deps "SubDirPkg" "`subDir`"
+    expectSelectionError deps "TableGit" "table-valued `git`"
+
+    let cfsg ← requiresFor root deps "LeanEval.Cfsg"
+    expectEq "imported extra require precedes mathlib; Cli is not required"
+      (names cfsg) "#[TauCeti, mathlib]"
+    let cfsgLakefile := lakefileToml "cfsg" cfsg (withChallengeDeps := false)
+    unless (cfsgLakefile.splitOn
+        (requireBlock "TauCeti" "https://github.com/TauCetiProject/TauCeti" tauCetiRev ++
+          mathlibBlock)).length == 2 do
+      throw <| IO.userError
+        s!"TauCeti require is not immediately before mathlib:\n{cfsgLakefile}"
+    if (cfsgLakefile.splitOn "Cli").length > 1 then
+      throw <| IO.userError s!"unimported Cli require was emitted:\n{cfsgLakefile}"
+
+    let plain ← requiresFor root deps "LeanEval.Plain"
+    expectEq "mathlib-only requires" (names plain) "#[mathlib]"
+    expectEq "mathlib-only lakefile"
+      (lakefileToml "plain" plain (withChallengeDeps := false))
+      (mathlibOnlyLakefile "plain")
+    -- A bare mathlib pin (the pre-existing API) coerces to the same result.
+    expectEq "coerced mathlib pin"
+      (lakefileToml "plain" (← IO.ofExcept (workspaceRequires deps.mathlib #["TauCeti.X"]))
+        (withChallengeDeps := false))
+      (mathlibOnlyLakefile "plain")
+
+    -- Values are TOML-escaped; ordinary values are emitted verbatim.
+    expectEq "plain TOML string" (tomlBasicString "https://x.org/a-b_c.git")
+      "\"https://x.org/a-b_c.git\""
+    expectEq "escaped TOML string" (tomlBasicString "a\"b\\c\nd\x01")
+      "\"a\\\"b\\\\c\\nd\\u0001\""
+    let odd : DependencySpec := { name := "Odd", git := "https://x.org/\"q\"", rev := "r\\1" }
+    unless ((lakefileToml "odd" #[odd] (withChallengeDeps := false)).splitOn
+        "git = \"https://x.org/\\\"q\\\"\"\nrev = \"r\\\\1\"\n").length == 2 do
+      throw <| IO.userError "lakefile require values are not TOML-escaped"
+
+    -- Generation rejects a mathlib require that a workspace would not
+    -- reproduce faithfully; the legacy mathlib loader still ignores the field.
+    let subDirRoot := root / "subdir-mathlib"
+    IO.FS.createDirAll subDirRoot
+    IO.FS.writeFile (subDirRoot / "lakefile.toml") <|
+      "name = \"fixture\"\n\n" ++ mathlibBlock.dropEnd 1 ++ "subDir = \"x\"\n"
+    match ← (loadRootDependencies subDirRoot).toBaseIO with
+    | .ok _ => throw <| IO.userError "mathlib require with `subDir` was accepted"
+    | .error e =>
+        unless ((toString e).splitOn "`subDir`").length > 1 do
+          throw <| IO.userError s!"unexpected mathlib `subDir` error: {e}"
+    expectEq "legacy loader ignores mathlib subDir"
+      (← loadRootMathlibDependency subDirRoot).rev mathlibRev
+
+    -- The workspace name is emitted as a TOML string too.
+    unless ((lakefileToml "a\"b" #[] (withChallengeDeps := false)).startsWith
+        "name = \"a\\\"b\"\n") do
+      throw <| IO.userError "workspace name is not TOML-escaped"
+  finally
+    IO.FS.removeDirAll root
+  IO.println "dependency tests passed"
diff --git a/lakefile.toml b/lakefile.toml
index 6fea374..ce074cb 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -14,3 +14,7 @@ root = "LeanEvalGenerator.Main"
 [[lean_exe]]
 name = "test_module_paths"
 root = "Tests.ModulePaths"
+
+[[lean_exe]]
+name = "test_dependencies"
+root = "Tests.Dependencies"
diff --git a/schemas/request-v1.schema.json b/schemas/request-v1.schema.json
index 10fee8b..3c80161 100644
--- a/schemas/request-v1.schema.json
+++ b/schemas/request-v1.schema.json
@@ -17,6 +17,10 @@
     "contextRoot": { "type": "string", "minLength": 1 },
     "leanToolchain": { "type": "string", "minLength": 1 },
     "mathlib": { "$ref": "#/$defs/dependency" },
+    "dependencies": {
+      "type": "array",
+      "items": { "$ref": "#/$defs/extraDependency" }
+    },
     "templates": {
       "type": "object",
       "additionalProperties": false,
@@ -40,6 +44,16 @@
         "rev": { "type": "string", "minLength": 1 }
       }
     },
+    "extraDependency": {
+      "type": "object",
+      "additionalProperties": false,
+      "required": ["name", "git", "rev"],
+      "properties": {
+        "name": { "type": "string", "minLength": 1, "not": { "const": "mathlib" } },
+        "git": { "type": "string", "minLength": 1 },
+        "rev": { "type": "string", "minLength": 1 }
+      }
+    },
     "resolvedHole": {
       "type": "object",
       "additionalProperties": false,
@@ -92,7 +106,7 @@
         "resolvedHoles"
       ],
       "properties": {
-        "id": { "type": "string", "minLength": 1 },
+        "id": { "type": "string", "pattern": "^[A-Za-z0-9][A-Za-z0-9_-]*$" },
         "title": { "type": "string", "minLength": 1 },
         "group": {
           "enum": ["formalization-evaluation", "software-verification", "open-conjectures"]
diff --git a/tests/scripts/contract.py b/tests/scripts/contract.py
index f10ee9e..bd003d7 100644
--- a/tests/scripts/contract.py
+++ b/tests/scripts/contract.py
@@ -69,6 +69,54 @@ def assert_rejected(payload: dict[str, object], message: str) -> None:
     assert message in result.stderr, result.stderr
 
 
+def lakefile_for(payload: dict[str, object]) -> str:
+    result = invoke(json.dumps(payload))
+    assert result.returncode == 0, result.stderr
+    files = json.loads(result.stdout)["files"]
+    [lakefile] = [item["content"] for item in files if item["path"] == "lakefile.toml"]
+    return lakefile
+
+
+def check_extra_dependencies() -> None:
+    """Render a problem importing a non-Mathlib package through the CLI."""
+    mathlib = '[[require]]\nname = "mathlib"\ngit = "x"\nrev = "y"\n\n'
+    tauceti = '[[require]]\nname = "TauCeti"\ngit = "https://t.example"\nrev = "abc"\n\n'
+    dependencies = [
+        {"name": "TauCeti", "git": "https://t.example", "rev": "abc"},
+        {"name": "Cli", "git": "https://c.example", "rev": "def"},
+    ]
+    with tempfile.TemporaryDirectory() as directory:
+        context = Path(directory)
+        ilean = context / ".lake/build/lib/lean"
+        ilean.mkdir(parents=True)
+        for module, header in [
+            ("WithTauCeti", "import TauCeti.GroupTheory.Classification\n\n"),
+            ("MathlibOnly", "import Mathlib.Logic.Basic\n\n"),
+        ]:
+            content = header + "theorem fixture : True := by sorry\n"
+            (context / f"{module}.lean").write_text(content, encoding="utf-8")
+            (ilean / f"{module}.ilean").write_text('{"decls": {}}', encoding="utf-8")
+            fixture = problem()
+            fixture["moduleName"] = module
+            fixture["moduleContent"] = content
+            hole = fixture["resolvedHoles"][0]
+            hole["module"] = module
+            hole["declarationName"] = "fixture"
+            hole["startLine"] = hole["endLine"] = 3
+            payload = request_with(fixture)
+            payload["contextRoot"] = str(context)
+            baseline = lakefile_for(payload)
+            payload["dependencies"] = dependencies
+            lakefile = lakefile_for(payload)
+            assert "Cli" not in lakefile, lakefile
+            if module == "WithTauCeti":
+                assert baseline.count("[[require]]") == 1, baseline
+                assert tauceti + mathlib in lakefile, lakefile
+                assert lakefile.count("[[require]]") == 2, lakefile
+            else:
+                assert lakefile == baseline, lakefile
+
+
 def main() -> int:
     subprocess.run(["lake", "build"], cwd=ROOT, check=True)
     subprocess.run(
@@ -152,6 +200,23 @@ def main() -> int:
         assert str(expected_ilean) in result.stderr, result.stderr
         assert "Arxiv/«0912/2382»" not in result.stderr
 
+    extra_named_mathlib = request_with(problem())
+    extra_named_mathlib["dependencies"] = [{"name": "mathlib", "git": "x", "rev": "y"}]
+    assert_rejected(extra_named_mathlib, "must not contain `mathlib`")
+
+    dependency_unknown = request_with(problem())
+    dependency_unknown["dependencies"] = [
+        {"name": "TauCeti", "git": "x", "rev": "y", "subDir": "z"}
+    ]
+    assert_rejected(dependency_unknown, "dependency contains an unknown field")
+
+    for bad_id in ["", "-leading", 'a"b', "a b", "a\\b", "a.b", "é"]:
+        invalid_id = problem()
+        invalid_id["id"] = bad_id
+        assert_rejected(request_with(invalid_id), "is invalid")
+
+    check_extra_dependencies()
+
     print("PASS schema errors stay off stdout and quoted source/ilean paths resolve")
     return 0