diff --git a/frontend/src/app/browse/[...slug]/page.tsx b/frontend/src/app/browse/[...slug]/page.tsx
index 70f7e19..c95f5ee 100644
--- a/frontend/src/app/browse/[...slug]/page.tsx
+++ b/frontend/src/app/browse/[...slug]/page.tsx
@@ -5,10 +5,13 @@ import { getModuleDeclarations, listModules } from "@/lib/api";
 import DeclarationItem from "@/components/DeclarationItem";
 import Header from "@/components/Header";
 import Footer from "@/components/Footer";
-import type { ModuleInfo } from "@/types";
+import BrowseSidebar from "@/components/BrowseSidebar";
+import MobileKindFilter from "@/components/MobileKindFilter";
+import type { ModuleInfo, DeclarationKind } from "@/types";
 
 interface Props {
   params: Promise<{ slug: string[] }>;
+  searchParams: Promise<{ kinds?: string }>;
 }
 
 function getDirectChildren(
@@ -32,96 +35,138 @@ function getDirectChildren(
     .sort((a, b) => a.name.localeCompare(b.name));
 }
 
-export default async function ModulePage({ params }: Props) {
+export default async function ModulePage({ params, searchParams }: Props) {
   const { slug } = await params;
+  const { kinds: kindsParam } = await searchParams;
   const moduleName = slug;
 
+  const selectedKinds = kindsParam
+    ? (kindsParam.split(",").filter(Boolean) as DeclarationKind[])
+    : [];
+  const kindsQuery = kindsParam ? `?kinds=${kindsParam}` : "";
+
   const [declarations, allModules] = await Promise.all([
     getModuleDeclarations(moduleName),
     listModules(),
   ]);
 
   const subModules = getDirectChildren(allModules, moduleName);
+  const moduleDocstring = allModules.find(
+    (m) => m.name.length === moduleName.length && m.name.every((p, i) => p === moduleName[i])
+  )?.docstring ?? null;
+
+  const filteredDeclarations =
+    selectedKinds.length > 0
+      ? declarations.filter((d) => selectedKinds.includes(d.kind))
+      : declarations;
 
   return (
     <div className="min-h-screen flex flex-col">
       <Header currentPath="browse" />
 
-      <main className="flex-1 max-w-3xl mx-auto w-full px-6 pt-24 pb-10">
-        <nav className="flex items-center gap-1.5 text-sm text-foreground/40 mb-6 flex-wrap">
-          <Link href="/browse" className="hover:text-foreground/70 transition-colors">
-            Browse
-          </Link>
-          {moduleName.map((part, i) => (
-            <span key={i} className="flex items-center gap-1.5">
-              <span>›</span>
-              {i < moduleName.length - 1 ? (
-                <Link
-                  href={`/browse/${moduleName.slice(0, i + 1).join("/")}`}
-                  className="hover:text-foreground/70 transition-colors"
-                >
-                  {part}
-                </Link>
-              ) : (
-                <span className="text-foreground/80 font-medium">{part}</span>
-              )}
-            </span>
-          ))}
-        </nav>
-
-        <div className="mb-6">
-          <h1 className="text-2xl font-bold tracking-tight font-mono">
-            {moduleName.join(".")}
-          </h1>
-          <p className="text-foreground/40 text-sm mt-1">
-            {declarations.length} declaration{declarations.length !== 1 ? "s" : ""}
-            {subModules.length > 0 &&
-              ` · ${subModules.length} submodule${subModules.length !== 1 ? "s" : ""}`}
-          </p>
-        </div>
+      <main className="flex-1 max-w-6xl mx-auto w-full px-5 sm:px-6 pt-24 pb-10">
+        <div className="flex gap-10">
+          <BrowseSidebar
+            modules={allModules}
+            showKindFilter
+            currentKinds={selectedKinds}
+          />
 
-        {subModules.length > 0 && (
-          <div className="mb-8">
-            <h2 className="text-xs font-semibold text-foreground/40 uppercase tracking-widest mb-3">
-              Submodules
-            </h2>
-            <div className="border border-foreground/10 rounded-xl overflow-hidden">
-              {subModules.map((sub, i) => (
-                <Link
-                  key={i}
-                  href={`/browse/${sub.fullPath.join("/")}`}
-                  className="flex items-center justify-between px-4 py-3 hover:bg-foreground/5 transition-colors border-b border-foreground/10 last:border-0 group"
-                >
-                  <span className="font-mono text-sm text-foreground/80 group-hover:text-foreground transition-colors">
-                    {sub.name}
-                  </span>
-                  <span className="text-xs text-foreground/35 tabular-nums">
-                    {sub.count}
-                  </span>
-                </Link>
+          <div className="flex-1 min-w-0">
+            <nav className="flex items-center gap-1.5 text-sm text-foreground/40 mb-6 flex-wrap">
+              <Link
+                href={`/browse${kindsQuery}`}
+                className="hover:text-foreground/70 transition-colors"
+              >
+                Browse
+              </Link>
+              {moduleName.map((part, i) => (
+                <span key={i} className="flex items-center gap-1.5">
+                  <span>›</span>
+                  {i < moduleName.length - 1 ? (
+                    <Link
+                      href={`/browse/${moduleName.slice(0, i + 1).join("/")}${kindsQuery}`}
+                      className="hover:text-foreground/70 transition-colors"
+                    >
+                      {part}
+                    </Link>
+                  ) : (
+                    <span className="text-foreground/80 font-medium">{part}</span>
+                  )}
+                </span>
               ))}
+            </nav>
+
+            <MobileKindFilter
+              pathname={`/browse/${moduleName.join("/")}`}
+              currentKinds={selectedKinds}
+            />
+
+            <div className="mb-6">
+              <h1 className="text-2xl font-bold tracking-tight font-mono break-all">
+                {moduleName.join(".")}
+              </h1>
+              {moduleDocstring && (
+                <p className="text-foreground/70 text-sm mt-2 leading-relaxed whitespace-pre-wrap">
+                  {moduleDocstring}
+                </p>
+              )}
+              <p className="text-foreground/40 text-sm mt-1">
+                {filteredDeclarations.length} declaration
+                {filteredDeclarations.length !== 1 ? "s" : ""}
+                {selectedKinds.length > 0 &&
+                  ` (filtered from ${declarations.length})`}
+                {subModules.length > 0 &&
+                  ` · ${subModules.length} submodule${subModules.length !== 1 ? "s" : ""}`}
+              </p>
             </div>
-          </div>
-        )}
 
-        {declarations.length > 0 && (
-          <div>
             {subModules.length > 0 && (
-              <h2 className="text-xs font-semibold text-foreground/40 uppercase tracking-widest mb-3">
-                Declarations
-              </h2>
+              <div className="mb-8">
+                <h2 className="text-xs font-semibold text-foreground/40 uppercase tracking-widest mb-3">
+                  Submodules
+                </h2>
+                <div className="border border-foreground/10 rounded-xl overflow-hidden">
+                  {subModules.map((sub, i) => (
+                    <Link
+                      key={i}
+                      href={`/browse/${sub.fullPath.join("/")}${kindsQuery}`}
+                      className="flex items-center justify-between gap-3 px-4 py-3 hover:bg-foreground/5 transition-colors border-b border-foreground/10 last:border-0 group"
+                    >
+                      <span className="font-mono text-sm text-foreground/80 group-hover:text-foreground transition-colors truncate">
+                        {sub.name}
+                      </span>
+                      <span className="text-xs text-foreground/35 tabular-nums shrink-0">
+                        {sub.count}
+                      </span>
+                    </Link>
+                  ))}
+                </div>
+              </div>
+            )}
+
+            {filteredDeclarations.length > 0 && (
+              <div>
+                {subModules.length > 0 && (
+                  <h2 className="text-xs font-semibold text-foreground/40 uppercase tracking-widest mb-3">
+                    Declarations
+                  </h2>
+                )}
+                {filteredDeclarations.map((decl, i) => (
+                  <DeclarationItem key={i} record={decl} />
+                ))}
+              </div>
             )}
-            {declarations.map((decl, i) => (
-              <DeclarationItem key={i} record={decl} />
-            ))}
-          </div>
-        )}
 
-        {subModules.length === 0 && declarations.length === 0 && (
-          <p className="text-foreground/40 text-sm">
-            No declarations found in this module.
-          </p>
-        )}
+            {subModules.length === 0 && filteredDeclarations.length === 0 && (
+              <p className="text-foreground/40 text-sm">
+                {selectedKinds.length > 0
+                  ? "No declarations match the current filter."
+                  : "No declarations found in this module."}
+              </p>
+            )}
+          </div>
+        </div>
       </main>
 
       <Footer />
diff --git a/frontend/src/app/browse/page.tsx b/frontend/src/app/browse/page.tsx
index 486560e..214e4ec 100644
--- a/frontend/src/app/browse/page.tsx
+++ b/frontend/src/app/browse/page.tsx
@@ -2,12 +2,13 @@ export const dynamic = "force-dynamic";
 
 import Link from "next/link";
 import { listModules } from "@/lib/api";
-import type { ModuleInfo } from "@/types";
+import type { ModuleInfo, DeclarationKind } from "@/types";
 import Header from "@/components/Header";
 import Footer from "@/components/Footer";
+import BrowseSidebar from "@/components/BrowseSidebar";
 
-function moduleUrl(name: string[]): string {
-  return `/browse/${name.join("/")}`;
+interface Props {
+  searchParams: Promise<{ kinds?: string }>;
 }
 
 function groupByTopLevel(modules: ModuleInfo[]): Map<string, ModuleInfo[]> {
@@ -20,7 +21,13 @@ function groupByTopLevel(modules: ModuleInfo[]): Map<string, ModuleInfo[]> {
   return groups;
 }
 
-export default async function BrowsePage() {
+export default async function BrowsePage({ searchParams }: Props) {
+  const { kinds: kindsParam } = await searchParams;
+  const selectedKinds = kindsParam
+    ? (kindsParam.split(",").filter(Boolean) as DeclarationKind[])
+    : [];
+  const kindsQuery = kindsParam ? `?kinds=${kindsParam}` : "";
+
   const modules = await listModules();
   const groups = groupByTopLevel(modules);
   const total = modules.reduce((s, m) => s + m.count, 0);
@@ -29,36 +36,44 @@ export default async function BrowsePage() {
     <div className="min-h-screen flex flex-col">
       <Header currentPath="browse" />
 
-      <main className="flex-1 max-w-3xl mx-auto w-full px-6 pt-24 pb-12">
-        <div className="mb-8">
-          <h1 className="text-3xl font-bold tracking-tight mb-2">Browse</h1>
-          <p className="text-foreground/50 text-sm">
-            {modules.length} modules · {total.toLocaleString()} declarations
-          </p>
-        </div>
+      <main className="flex-1 max-w-6xl mx-auto w-full px-5 sm:px-6 pt-24 pb-12">
+        <div className="flex gap-10">
+          <BrowseSidebar modules={modules} currentKinds={selectedKinds} />
+
+          <div className="flex-1 min-w-0">
+            <div className="mb-8">
+              <h1 className="text-3xl font-bold tracking-tight mb-2">Browse</h1>
+              <p className="text-foreground/50 text-sm">
+                {modules.length} modules · {total.toLocaleString()} declarations
+              </p>
+            </div>
 
-        <div className="flex flex-col gap-8">
-          {Array.from(groups.entries()).map(([top, mods]) => (
-            <section key={top}>
-              <h2 className="text-xs font-semibold text-foreground/40 uppercase tracking-widest mb-3 font-mono">
-                {top}
-              </h2>
-              <div className="border border-foreground/10 rounded-xl overflow-hidden">
-                {mods.map((m, i) => (
-                  <Link
-                    key={i}
-                    href={moduleUrl(m.name)}
-                    className="flex items-center justify-between px-4 py-3 hover:bg-foreground/5 transition-colors border-b border-foreground/10 last:border-0 group"
-                  >
-                    <span className="font-mono text-sm text-foreground/80 group-hover:text-foreground transition-colors">
-                      {m.name.join(".")}
-                    </span>
-                    <span className="text-xs text-foreground/35 tabular-nums">{m.count}</span>
-                  </Link>
-                ))}
-              </div>
-            </section>
-          ))}
+            <div className="flex flex-col gap-8">
+              {Array.from(groups.entries()).map(([top, mods]) => (
+                <section key={top}>
+                  <h2 className="text-xs font-semibold text-foreground/40 uppercase tracking-widest mb-3 font-mono">
+                    {top}
+                  </h2>
+                  <div className="border border-foreground/10 rounded-xl overflow-hidden">
+                    {mods.map((m, i) => (
+                      <Link
+                        key={i}
+                        href={`/browse/${m.name.join("/")}${kindsQuery}`}
+                        className="flex items-center justify-between gap-3 px-4 py-3 hover:bg-foreground/5 transition-colors border-b border-foreground/10 last:border-0 group"
+                      >
+                        <span className="font-mono text-sm text-foreground/80 group-hover:text-foreground transition-colors truncate">
+                          {m.name.join(".")}
+                        </span>
+                        <span className="text-xs text-foreground/35 tabular-nums shrink-0">
+                          {m.count}
+                        </span>
+                      </Link>
+                    ))}
+                  </div>
+                </section>
+              ))}
+            </div>
+          </div>
         </div>
       </main>
 
diff --git a/frontend/src/app/globals.css b/frontend/src/app/globals.css
index 42e612d..3ad4db1 100644
--- a/frontend/src/app/globals.css
+++ b/frontend/src/app/globals.css
@@ -6,3 +6,18 @@
   margin: 0.5em 0;
   overflow-x: auto;
 }
+
+.thin-scrollbar {
+  scrollbar-width: thin;
+  scrollbar-color: rgb(127 127 127 / 0.2) transparent;
+}
+
+.thin-scrollbar::-webkit-scrollbar {
+  width: 3px;
+  height: 3px;
+}
+
+.thin-scrollbar::-webkit-scrollbar-thumb {
+  background: rgb(127 127 127 / 0.2);
+  border-radius: 9999px;
+}
diff --git a/frontend/src/components/BrowseSidebar.tsx b/frontend/src/components/BrowseSidebar.tsx
new file mode 100644
index 0000000..36e8feb
--- /dev/null
+++ b/frontend/src/components/BrowseSidebar.tsx
@@ -0,0 +1,227 @@
+"use client";
+
+import { useState } from "react";
+import Link from "next/link";
+import { usePathname, useRouter } from "next/navigation";
+import type { ModuleInfo, DeclarationKind } from "@/types";
+
+const ALL_KINDS: DeclarationKind[] = [
+  "theorem",
+  "definition",
+  "structure",
+  "inductive",
+  "classInductive",
+  "instance",
+  "abbrev",
+  "axiom",
+  "opaque",
+  "proofWanted",
+];
+
+const KIND_LABELS: Partial<Record<DeclarationKind, string>> = {
+  theorem: "Theorem",
+  definition: "Definition",
+  structure: "Structure",
+  inductive: "Inductive",
+  classInductive: "Class",
+  instance: "Instance",
+  abbrev: "Abbreviation",
+  axiom: "Axiom",
+  opaque: "Opaque",
+  proofWanted: "Proof Wanted",
+};
+
+interface Props {
+  modules: ModuleInfo[];
+  showKindFilter?: boolean;
+  currentKinds?: DeclarationKind[];
+}
+
+function getSubmodules(modules: ModuleInfo[], lib: string) {
+  const subMap = new Map<string, number>();
+  for (const m of modules) {
+    if (m.name[0] === lib && m.name.length > 1) {
+      const sub = m.name[1];
+      subMap.set(sub, (subMap.get(sub) ?? 0) + m.count);
+    }
+  }
+  return Array.from(subMap.entries())
+    .map(([name, count]) => ({ name, fullPath: [lib, name], count }))
+    .sort((a, b) => a.name.localeCompare(b.name));
+}
+
+function displayName(lib: string) {
+  if (lib === "QuantumInfo") return "Quantum Info";
+  return lib;
+}
+
+export default function BrowseSidebar({
+  modules,
+  showKindFilter,
+  currentKinds = [],
+}: Props) {
+  const pathname = usePathname();
+  const router = useRouter();
+
+  const topLevelNames = Array.from(
+    new Set(modules.map((m) => m.name[0]).filter(Boolean))
+  ).sort();
+
+  const initialExpanded = new Set(
+    topLevelNames.filter((lib) => pathname.startsWith(`/browse/${lib}`))
+  );
+  const [expandedLibs, setExpandedLibs] = useState<Set<string>>(initialExpanded);
+
+  function toggleLib(lib: string) {
+    setExpandedLibs((prev) => {
+      const next = new Set(prev);
+      if (next.has(lib)) next.delete(lib);
+      else next.add(lib);
+      return next;
+    });
+  }
+
+  function toggleKind(kind: DeclarationKind) {
+    const isVisible = currentKinds.length === 0 || currentKinds.includes(kind);
+
+    let newKinds: DeclarationKind[];
+    if (isVisible) {
+      newKinds =
+        currentKinds.length === 0
+          ? ALL_KINDS.filter((k) => k !== kind)
+          : currentKinds.filter((k) => k !== kind);
+    } else {
+      newKinds = [...currentKinds, kind];
+    }
+
+    const isAll = newKinds.length === 0 || newKinds.length === ALL_KINDS.length;
+    router.replace(isAll ? pathname : `${pathname}?kinds=${newKinds.join(",")}`);
+  }
+
+  const kindsQuery =
+    currentKinds.length > 0 ? `?kinds=${currentKinds.join(",")}` : "";
+
+  return (
+    <aside className="w-52 shrink-0 sticky top-24 self-start hidden lg:block max-h-[calc(100vh-6rem)] overflow-y-auto pr-1 thin-scrollbar">
+      {/* Library tree */}
+      <div className="mb-6">
+        <p className="text-xs font-semibold text-foreground/40 uppercase tracking-widest mb-3">
+          Libraries
+        </p>
+        <div className="flex flex-col gap-0.5">
+          <Link
+            href={`/browse${kindsQuery}`}
+            className={`text-sm px-3 py-1.5 rounded-lg transition-colors ${
+              pathname === "/browse"
+                ? "bg-foreground/10 text-foreground font-medium"
+                : "text-foreground/60 hover:text-foreground hover:bg-foreground/5"
+            }`}
+          >
+            All
+          </Link>
+
+          {topLevelNames.map((lib) => {
+            const submodules = getSubmodules(modules, lib);
+            const isOnLib =
+              pathname === `/browse/${lib}` ||
+              pathname.startsWith(`/browse/${lib}/`);
+            const isExpanded = expandedLibs.has(lib);
+
+            return (
+              <div key={lib}>
+                <div className="flex items-center gap-1">
+                  <Link
+                    href={`/browse/${lib}${kindsQuery}`}
+                    className={`flex-1 text-sm px-3 py-1.5 rounded-lg transition-colors ${
+                      isOnLib
+                        ? "bg-foreground/10 text-foreground font-medium"
+                        : "text-foreground/60 hover:text-foreground hover:bg-foreground/5"
+                    }`}
+                  >
+                    {displayName(lib)}
+                  </Link>
+                  {submodules.length > 0 && (
+                    <button
+                      onClick={() => toggleLib(lib)}
+                      className="p-1.5 text-foreground/30 hover:text-foreground/60 transition-colors text-xs leading-none"
+                      aria-label={isExpanded ? "Collapse" : "Expand"}
+                    >
+                      {isExpanded ? "▾" : "▸"}
+                    </button>
+                  )}
+                </div>
+
+                {isExpanded && submodules.length > 0 && (
+                  <div className="ml-4 mt-0.5 mb-1 flex flex-col gap-0.5 border-l border-foreground/10 pl-3">
+                    {submodules.map((sub) => {
+                      const isActive =
+                        pathname === `/browse/${sub.fullPath.join("/")}` ||
+                        pathname.startsWith(`/browse/${sub.fullPath.join("/")}/`);
+                      return (
+                        <Link
+                          key={sub.name}
+                          href={`/browse/${sub.fullPath.join("/")}${kindsQuery}`}
+                          className={`text-xs py-1 px-2 rounded transition-colors flex items-center justify-between gap-2 ${
+                            isActive
+                              ? "bg-foreground/10 text-foreground font-medium"
+                              : "text-foreground/50 hover:text-foreground/80 hover:bg-foreground/5"
+                          }`}
+                        >
+                          <span className="font-mono truncate">{sub.name}</span>
+                          <span className="text-foreground/30 tabular-nums shrink-0">
+                            {sub.count}
+                          </span>
+                        </Link>
+                      );
+                    })}
+                  </div>
+                )}
+              </div>
+            );
+          })}
+        </div>
+      </div>
+
+      {/* Kind filter */}
+      {showKindFilter && (
+        <div>
+          <div className="flex items-center justify-between mb-3">
+            <p className="text-xs font-semibold text-foreground/40 uppercase tracking-widest">
+              Filter by Kind
+            </p>
+            {currentKinds.length > 0 && (
+              <button
+                onClick={() => router.replace(pathname)}
+                className="text-xs text-foreground/40 hover:text-foreground/60 transition-colors"
+              >
+                Reset
+              </button>
+            )}
+          </div>
+          <div className="flex flex-col gap-0.5">
+            {ALL_KINDS.map((kind) => {
+              const isVisible =
+                currentKinds.length === 0 || currentKinds.includes(kind);
+              return (
+                <label
+                  key={kind}
+                  className="flex items-center gap-2 px-2 py-1.5 rounded-lg cursor-pointer hover:bg-foreground/5 transition-colors"
+                >
+                  <input
+                    type="checkbox"
+                    checked={isVisible}
+                    onChange={() => toggleKind(kind)}
+                    className="w-3.5 h-3.5 accent-blue-400 cursor-pointer"
+                  />
+                  <span className="text-sm text-foreground/60">
+                    {KIND_LABELS[kind] ?? kind}
+                  </span>
+                </label>
+              );
+            })}
+          </div>
+        </div>
+      )}
+    </aside>
+  );
+}
diff --git a/frontend/src/components/DeclarationItem.tsx b/frontend/src/components/DeclarationItem.tsx
index 88a4526..2d9531a 100644
--- a/frontend/src/components/DeclarationItem.tsx
+++ b/frontend/src/components/DeclarationItem.tsx
@@ -41,35 +41,37 @@ export default function DeclarationItem({ record }: Props) {
         </span>
         <div className="flex-1 min-w-0">
           <div className="flex items-start justify-between gap-2">
-            <h3 className="font-semibold text-base leading-snug">
+            <h3 className="font-semibold text-base leading-snug min-w-0 break-words">
               <LatexText text={record.informal_name} />
             </h3>
             <a
               href={docUrl(record.module_name, record.name)}
               target="_blank"
               rel="noopener noreferrer"
-              className="text-xs text-foreground/30 hover:text-foreground/60 font-mono shrink-0 mt-0.5"
+              className="text-xs text-foreground/30 hover:text-foreground/60 font-mono shrink-0 mt-0.5 hidden sm:block"
             >
               #{anchor}
             </a>
           </div>
 
-          <p className="mt-1.5 text-sm text-foreground/70 leading-relaxed">
+          <p className="mt-1.5 text-sm text-foreground/70 leading-relaxed break-words">
             <LatexText text={record.informal_description} />
           </p>
 
           <div className="mt-3">
             <button
               onClick={() => setExpanded((v) => !v)}
-              className="text-xs text-foreground/35 hover:text-foreground/60 transition-colors flex items-center gap-1"
+              className="text-xs text-foreground/35 hover:text-foreground/60 transition-colors flex items-start gap-1 text-left max-w-full"
             >
-              <span>{expanded ? "▾" : "▸"}</span>
-              <span className="font-mono">{record.name.join(".")}</span>
+              <span className="shrink-0">{expanded ? "▾" : "▸"}</span>
+              <span className="font-mono break-all min-w-0">{record.name.join(".")}</span>
             </button>
             {expanded && (
-              <pre className="mt-2 p-3 bg-foreground/5 rounded-lg text-xs font-mono overflow-x-auto text-foreground/65 border border-foreground/10 leading-relaxed whitespace-pre-wrap">
+              <pre className="mt-2 p-3 bg-foreground/5 rounded-lg text-xs font-mono overflow-x-auto text-foreground/65 border border-foreground/10 leading-relaxed whitespace-pre-wrap break-words">
                 {record.signature}
-                {record.value != null && `\n:=\n${record.value}`}
+                {record.value
+                  ? `\n${record.value.trimStart().startsWith(":=") ? record.value : `:= ${record.value}`}`
+                  : ""}
               </pre>
             )}
           </div>
diff --git a/frontend/src/components/LatexText.tsx b/frontend/src/components/LatexText.tsx
index bdc7502..0648305 100644
--- a/frontend/src/components/LatexText.tsx
+++ b/frontend/src/components/LatexText.tsx
@@ -14,8 +14,8 @@ type Part =
 
 function parseParts(text: string): Part[] {
   const parts: Part[] = [];
-  // Match $$...$$ first (display), then $...$ (inline)
-  const re = /(\$\$[\s\S]*?\$\$|\$[^$\n]+?\$)/g;
+  // Match $$...$$, \[...\] (display), then \(...\), $...$ (inline)
+  const re = /(\$\$[\s\S]*?\$\$|\\\[[\s\S]*?\\\]|\\\([\s\S]*?\\\)|\$[^$\n]+?\$)/g;
   let last = 0;
   let match: RegExpExecArray | null;
 
@@ -26,6 +26,10 @@ function parseParts(text: string): Part[] {
     const raw = match[0];
     if (raw.startsWith("$$")) {
       parts.push({ type: "block", latex: raw.slice(2, -2) });
+    } else if (raw.startsWith("\\[")) {
+      parts.push({ type: "block", latex: raw.slice(2, -2) });
+    } else if (raw.startsWith("\\(")) {
+      parts.push({ type: "inline", latex: raw.slice(2, -2) });
     } else {
       parts.push({ type: "inline", latex: raw.slice(1, -1) });
     }
@@ -38,15 +42,46 @@ function parseParts(text: string): Part[] {
   return parts;
 }
 
+function escapeHtml(s: string): string {
+  return s
+    .replace(/&/g, "&amp;")
+    .replace(/</g, "&lt;")
+    .replace(/>/g, "&gt;")
+    .replace(/"/g, "&quot;")
+    .replace(/'/g, "&#39;");
+}
+
+const MATHBB_UNICODE: Record<string, string> = {
+  R: "ℝ", C: "ℂ", Z: "ℤ", N: "ℕ", Q: "ℚ",
+  P: "ℙ", H: "ℍ", F: "𝔽", K: "𝕂",
+};
+
+// The informal-description generator sometimes emits math-mode commands like
+// `\mathbb{R}` inside `\text{...}`, which KaTeX (correctly) refuses to render.
+// Replace those with their Unicode equivalents so the text renders cleanly.
+function sanitizeLatex(latex: string): string {
+  const textGroup = /\\text\{((?:[^{}]|\{[^{}]*\})*)\}/g;
+  return latex.replace(textGroup, (_match, inner: string) => {
+    const fixed = inner.replace(
+      /\\mathbb\{([A-Z])\}/g,
+      (m, letter: string) => MATHBB_UNICODE[letter] ?? m
+    );
+    return `\\text{${fixed}}`;
+  });
+}
+
 function renderLatex(latex: string, displayMode: boolean): string {
+  const source = sanitizeLatex(latex);
   try {
-    return katex.renderToString(latex, {
+    return katex.renderToString(source, {
       displayMode,
-      throwOnError: false,
+      throwOnError: true,
+      strict: "ignore",
       trust: false,
     });
   } catch {
-    return latex;
+    const [open, close] = displayMode ? ["\\[", "\\]"] : ["$", "$"];
+    return escapeHtml(`${open}${latex}${close}`);
   }
 }
 
diff --git a/frontend/src/components/MobileKindFilter.tsx b/frontend/src/components/MobileKindFilter.tsx
new file mode 100644
index 0000000..932c420
--- /dev/null
+++ b/frontend/src/components/MobileKindFilter.tsx
@@ -0,0 +1,83 @@
+"use client";
+
+import { useRouter } from "next/navigation";
+import type { DeclarationKind } from "@/types";
+
+const ALL_KINDS: DeclarationKind[] = [
+  "theorem",
+  "definition",
+  "structure",
+  "inductive",
+  "classInductive",
+  "instance",
+  "abbrev",
+  "axiom",
+  "opaque",
+  "proofWanted",
+];
+
+const KIND_LABELS: Partial<Record<DeclarationKind, string>> = {
+  theorem: "Theorem",
+  definition: "Definition",
+  structure: "Structure",
+  inductive: "Inductive",
+  classInductive: "Class",
+  instance: "Instance",
+  abbrev: "Abbrev",
+  axiom: "Axiom",
+  opaque: "Opaque",
+  proofWanted: "Proof Wanted",
+};
+
+interface Props {
+  pathname: string;
+  currentKinds: DeclarationKind[];
+}
+
+export default function MobileKindFilter({ pathname, currentKinds }: Props) {
+  const router = useRouter();
+
+  function toggleKind(kind: DeclarationKind) {
+    const isVisible = currentKinds.length === 0 || currentKinds.includes(kind);
+    let newKinds: DeclarationKind[];
+    if (isVisible) {
+      newKinds =
+        currentKinds.length === 0
+          ? ALL_KINDS.filter((k) => k !== kind)
+          : currentKinds.filter((k) => k !== kind);
+    } else {
+      newKinds = [...currentKinds, kind];
+    }
+    const isAll = newKinds.length === 0 || newKinds.length === ALL_KINDS.length;
+    router.replace(isAll ? pathname : `${pathname}?kinds=${newKinds.join(",")}`);
+  }
+
+  return (
+    <div className="lg:hidden flex items-center gap-1.5 overflow-x-auto pb-1 mb-5 -mx-5 sm:-mx-6 px-5 sm:px-6 thin-scrollbar">
+      {currentKinds.length > 0 && (
+        <button
+          onClick={() => router.replace(pathname)}
+          className="shrink-0 text-xs px-3 py-1 rounded-full border border-foreground/25 text-foreground/50 hover:text-foreground/80 transition-colors whitespace-nowrap"
+        >
+          Reset
+        </button>
+      )}
+      {ALL_KINDS.map((kind) => {
+        const isVisible = currentKinds.length === 0 || currentKinds.includes(kind);
+        return (
+          <button
+            key={kind}
+            onClick={() => toggleKind(kind)}
+            className={`shrink-0 text-xs px-3 py-1 rounded-full border transition-colors whitespace-nowrap ${
+              isVisible
+                ? "border-foreground/20 bg-foreground/8 text-foreground/70"
+                : "border-foreground/10 text-foreground/25"
+            }`}
+          >
+            {KIND_LABELS[kind] ?? kind}
+          </button>
+        );
+      })}
+    </div>
+  );
+}
diff --git a/frontend/src/types/index.ts b/frontend/src/types/index.ts
index 4ab5739..584d665 100644
--- a/frontend/src/types/index.ts
+++ b/frontend/src/types/index.ts
@@ -33,4 +33,5 @@ export interface QueryResult {
 export interface ModuleInfo {
   name: LeanName;
   count: number;
+  docstring: string | null;
 }
diff --git a/server.py b/server.py
index e1a24ca..23a5220 100644
--- a/server.py
+++ b/server.py
@@ -119,6 +119,7 @@ class UserFeedback(BaseModel):
 class ModuleInfo(BaseModel):
     name: LeanName
     count: int
+    docstring: str | None = None
 
 
 @app.get("/modules")
@@ -127,11 +128,12 @@ def list_modules(request: Request) -> list[ModuleInfo]:
     with app.pool.connection() as conn:
         with conn.cursor(row_factory=class_row(ModuleInfo)) as cursor:
             cursor.execute("""
-                SELECT d.module_name AS name, COUNT(*) AS count
+                SELECT d.module_name AS name, COUNT(*) AS count, mo.docstring
                 FROM declaration d
+                INNER JOIN module mo ON mo.name = d.module_name
                 WHERE d.visible = TRUE
                   AND EXISTS(SELECT 1 FROM informal i WHERE i.symbol_name = d.name)
-                GROUP BY d.module_name
+                GROUP BY d.module_name, mo.docstring
                 ORDER BY d.module_name
             """)
             return cursor.fetchall()