diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts
index ad73b918..49c54078 100644
--- a/src/lib/commons/types.ts
+++ b/src/lib/commons/types.ts
@@ -157,6 +157,7 @@ export type FunctorPropertyAssignment = Replace<
 >
 
 export type Lemma = {
+	id: string
 	title: string
 	claim: string
 	proof: string
diff --git a/src/routes/category-implications/+page.svelte b/src/routes/category-implications/+page.svelte
index 9e527ecd..387fa1d7 100644
--- a/src/routes/category-implications/+page.svelte
+++ b/src/routes/category-implications/+page.svelte
@@ -70,6 +70,11 @@
 	well.
 </p>
 
+<p class="hint">
+	In some cases, implications are a bit too rigid, which is why we also provide a small
+	collection of <a href="/lemmas">lemmas</a>.
+</p>
+
 <button class="button" onclick={toggle}>
 	{#if show_deduced_implications}
 		Hide deduced implications
diff --git a/src/routes/lemma/[id]/+page.server.ts b/src/routes/lemma/[id]/+page.server.ts
index 37c707e6..8d7b2029 100644
--- a/src/routes/lemma/[id]/+page.server.ts
+++ b/src/routes/lemma/[id]/+page.server.ts
@@ -3,20 +3,13 @@ import { batch, query } from '$lib/server/db.catdat'
 import { render_nested_formulas } from '$lib/server/rendering'
 import { error } from '@sveltejs/kit'
 import sql from 'sql-template-tag'
-import type { EntryGenerator } from './$types'
-
-export const entries: EntryGenerator = async () => {
-	const { rows, err } = query<{ id: string }>(sql`SELECT id FROM lemmas`)
-	if (err) throw new Error('Database error: Failed to load tags')
-	return rows
-}
 
 export const load = async (event) => {
 	const id = event.params.id
 
 	const { results, err } = batch<[Lemma, CategoryShort, { id: string }]>([
 		sql`
-        	SELECT title, claim, proof FROM lemmas WHERE id = ${id}
+        	SELECT id, title, claim, proof FROM lemmas WHERE id = ${id}
     	`,
 		sql`
 			SELECT c.id, c.name
diff --git a/src/routes/lemmas/+page.server.ts b/src/routes/lemmas/+page.server.ts
new file mode 100644
index 00000000..4ca149d5
--- /dev/null
+++ b/src/routes/lemmas/+page.server.ts
@@ -0,0 +1,15 @@
+import type { Lemma } from '$lib/commons/types'
+import { query } from '$lib/server/db.catdat'
+import { render_nested_formulas } from '$lib/server/rendering'
+import { error } from '@sveltejs/kit'
+import sql from 'sql-template-tag'
+
+export const load = async (event) => {
+	const { rows: lemmas, err } = query<Lemma>(
+		sql`SELECT id, title, claim, proof FROM lemmas ORDER BY lower(title)`,
+	)
+
+	if (err) error(500, 'Could not load lemmas')
+
+	return { lemmas }
+}
diff --git a/src/routes/lemmas/+page.svelte b/src/routes/lemmas/+page.svelte
new file mode 100644
index 00000000..1907cc3c
--- /dev/null
+++ b/src/routes/lemmas/+page.svelte
@@ -0,0 +1,24 @@
+<script lang="ts">
+	import MetaData from '$components/MetaData.svelte'
+	import SuggestionForm from '$components/SuggestionForm.svelte'
+
+	let { data } = $props()
+</script>
+
+<MetaData title="Lemmas" />
+
+<h2>Lemmas</h2>
+
+<p class="hint">
+	These are reusable lemmas used in multiple proofs of categorical properties in CatDat.
+</p>
+
+<ul>
+	{#each data.lemmas as lemma (lemma.id)}
+		<li>
+			<a href="/lemma/{lemma.id}">{lemma.title}</a>
+		</li>
+	{/each}
+</ul>
+
+<SuggestionForm />