diff --git a/shared/node/index.ts b/shared/node/index.ts
index 19308490..08e18c8b 100644
--- a/shared/node/index.ts
+++ b/shared/node/index.ts
@@ -50,3 +50,29 @@ export const execFileAsync = promisify(execFile)
 
 export * from './bwrap.ts'
 export * from './directories.ts'
+
+/**
+ * Turns an iterator into a ReadableStream.
+ * Node has had this as `ReadableStream.from` for years,
+ * but Next's TypeScript story expects us to always use the least-common-denominator of browser-available and node-available.
+ * (we should replace this with `ReadableStream.from` once typescript includes types for it).
+ *
+ * Adapted from
+ * https://developer.mozilla.org/en-US/docs/Web/API/ReadableStream#convert_an_iterator_or_async_iterator_to_a_stream
+ * which lacks the `cancel` function.
+ */
+export function iteratorToStream<T>(iterator: AsyncGenerator<T, void>): ReadableStream<T> {
+  return new ReadableStream({
+    async pull(controller) {
+      const { value, done } = await iterator.next()
+      if (done) {
+        controller.close()
+      } else {
+        controller.enqueue(value)
+      }
+    },
+    async cancel() {
+      await iterator.return()
+    },
+  })
+}
diff --git a/src/app/[userName]/ProjectRow.tsx b/src/app/[userName]/ProjectRow.tsx
index 6d2cf897..18a21b90 100644
--- a/src/app/[userName]/ProjectRow.tsx
+++ b/src/app/[userName]/ProjectRow.tsx
@@ -108,6 +108,7 @@ export function ProjectRow({
               <MenuItem onAction={() => setRenaming(true)} isDisabled={actionPending}>
                 Rename
               </MenuItem>
+              <MenuItem href={`/${username}/${encodeURIComponent(project.name)}/download`}>Download</MenuItem>
               <MenuItem
                 onAction={() => {
                   if (!confirm(`Delete project "${project.name}"? Project files will be kept.`)) return
diff --git a/src/app/[userName]/[projectName]/download/route.ts b/src/app/[userName]/[projectName]/download/route.ts
new file mode 100644
index 00000000..8b4e8f4e
--- /dev/null
+++ b/src/app/[userName]/[projectName]/download/route.ts
@@ -0,0 +1,53 @@
+import { spawn } from 'node:child_process'
+
+import { zProjectName, zUserName } from '@leanprover/workbench-shared'
+import { getProjectDir, iteratorToStream } from '@leanprover/workbench-shared/node'
+import { notFound } from 'next/navigation'
+import z from 'zod'
+
+import { requireAuth } from '@/lib/server/auth'
+import { getDb } from '@/lib/server/db'
+import { canAccessProject } from '@/lib/server/util'
+
+const zParams = z.object({
+  userName: zUserName,
+  projectName: zProjectName,
+})
+
+async function* generateProjectTgz(owner: { id: string }, projectId: string): AsyncGenerator<Uint8Array, void> {
+  const tar = spawn('tar', ['-czf', '-', '--exclude=./.lake', '.'], {
+    stdio: ['ignore', 'pipe', 'inherit'],
+    cwd: getProjectDir(owner, projectId),
+  })
+  const closed = new Promise(resolve => tar.on('close', resolve))
+  try {
+    yield* tar.stdout
+    const code = await closed
+    if (code !== 0) throw new Error(`tar of project ${owner.id}/${projectId} exited with ${code}`)
+  } finally {
+    tar.kill()
+  }
+}
+
+export async function GET(_req: Request, { params }: { params: Promise<unknown> }) {
+  const parsed = zParams.safeParse(await params)
+  if (!parsed.success) return new Response(parsed.error.issues[0]!.message, { status: 400 })
+  const { userName, projectName } = parsed.data
+
+  const session = await requireAuth()
+  const db = getDb()
+  const owner = await db.user.findUnique({ where: { name: userName } })
+  if (!owner) notFound()
+  const project = await db.project.findUnique({
+    where: { userId_name: { userId: owner.id, name: projectName } },
+  })
+  // 404 rather than 403 to avoid leaking the existence of inaccessible projects.
+  if (!project || !canAccessProject(session.user, project)) notFound()
+
+  return new Response(iteratorToStream(generateProjectTgz(owner, project.id)), {
+    headers: {
+      'Content-Type': 'application/gzip',
+      'Content-Disposition': `attachment; filename="${project.name}.tgz"`,
+    },
+  })
+}