diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 9d79088..ef495f5 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -12,6 +12,7 @@ import DocGen4.Output.Module
 import DocGen4.Output.NotFound
 import DocGen4.Output.Find
 import DocGen4.Output.SourceLinker
+import DocGen4.Output.Search
 import DocGen4.Output.ToJson
 import DocGen4.Output.FoundationalTypes
 import DocGen4.LeanInk.Process
@@ -35,11 +36,13 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let notFoundHtml := ReaderT.run notFound config |>.toString
   let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
   let navbarHtml := ReaderT.run navbar config |>.toString
+  let searchHtml := ReaderT.run search config |>.toString
   let docGenStatic := #[
     ("style.css", styleCss),
     ("declaration-data.js", declarationDataCenterJs),
     ("nav.js", navJs),
     ("how-about.js", howAboutJs),
+    ("search.html", searchHtml),
     ("search.js", searchJs),
     ("mathjax-config.js", mathjaxConfigJs),
     ("instances.js", instancesJs),
diff --git a/DocGen4/Output/Search.lean b/DocGen4/Output/Search.lean
new file mode 100644
index 0000000..b748c7e
--- /dev/null
+++ b/DocGen4/Output/Search.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2023 Jeremy Salwen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Salwen
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <|
+  pure <|
+    <main>
+      <a id="top"></a>
+      <h1> Search Results </h1>
+      <label for="search_page_query">Query:</label><input id="search_page_query" />
+      <script>
+        document.getElementById("search_page_query").value = new URL(window.location.href).searchParams.get("q")
+      </script>
+      <div id="search_results">
+      </div>
+    </main>
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index 2c7ea8a..f2b7409 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -45,10 +45,10 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
         <header>
           <h1><label for="nav_toggle"></label>Documentation</h1>
           <p class="header_filename break_within">{title}</p>
-          -- TODO: Replace this form with our own search
           <form action="https://google.com/search" method="get" id="search_form">
             <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"/>
             <input type="text" name="q" autocomplete="off"/>&#32;
+            <button onclick="javascript: form.action='/search.html';">Search</button>
             <button>Google site search</button>
           </form>
         </header>
diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean
index 01b3ba0..86d2be0 100644
--- a/DocGen4/Process/Hierarchy.lean
+++ b/DocGen4/Process/Hierarchy.lean
@@ -89,6 +89,7 @@ def baseDirBlackList : HashSet String :=
     "find",
     "how-about.js",
     "index.html",
+    "search.html",
     "foundational_types.html",
     "mathjax-config.js",
     "navbar.html",
diff --git a/lakefile.lean b/lakefile.lean
index 9a8b32f..f558b8b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -94,6 +94,7 @@ library_facet docs (lib) : FilePath := do
     basePath / "index.html",
     basePath / "404.html",
     basePath / "navbar.html",
+    basePath / "search.html",
     basePath / "find" / "index.html",
     basePath / "find" / "find.js",
     basePath / "src"  / "alectryon.css",
diff --git a/static/declaration-data.js b/static/declaration-data.js
index 953edf2..8c4e42c 100644
--- a/static/declaration-data.js
+++ b/static/declaration-data.js
@@ -67,7 +67,7 @@ export class DeclarationDataCenter {
    * Search for a declaration.
    * @returns {Array<any>}
    */
-  search(pattern, strict = true) {
+  search(pattern, strict = true, maxResults=undefined) {
     if (!pattern) {
       return [];
     }
@@ -75,7 +75,7 @@ export class DeclarationDataCenter {
       let decl = this.declarationData.declarations[pattern];
       return decl ? [decl] : [];
     } else {
-      return getMatches(this.declarationData.declarations, pattern);
+      return getMatches(this.declarationData.declarations, pattern, maxResults);
     }
   }
 
@@ -159,7 +159,7 @@ function matchCaseSensitive(declName, lowerDeclName, pattern) {
   }
 }
 
-function getMatches(declarations, pattern, maxResults = 30) {
+function getMatches(declarations, pattern, maxResults = undefined) {
   const lowerPats = pattern.toLowerCase().split(/\s/g);
   const patNoSpaces = pattern.replace(/\s/g, "");
   const results = [];
diff --git a/static/search.js b/static/search.js
index 074d8bc..835bfca 100644
--- a/static/search.js
+++ b/static/search.js
@@ -4,27 +4,36 @@
 
 import { DeclarationDataCenter } from "./declaration-data.js";
 
+// Search form and input in the upper right toolbar
 const SEARCH_FORM = document.querySelector("#search_form");
 const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]");
 
-// Create an `div#search_results` to hold all search results.
-let sr = document.createElement("div");
-sr.id = "search_results";
-SEARCH_FORM.appendChild(sr);
+// Search form on the /search.html_page.  These may be null.
+const SEARCH_PAGE_INPUT = document.querySelector("#search_page_query")
+const SEARCH_RESULTS = document.querySelector("#search_results")
+
+// Max results to show for autocomplete or /search.html page.
+const AC_MAX_RESULTS = 30
+const SEARCH_PAGE_MAX_RESULTS = undefined
+
+// Create an `div#autocomplete_results` to hold all autocomplete results.
+let ac_results = document.createElement("div");
+ac_results.id = "autocomplete_results";
+SEARCH_FORM.appendChild(ac_results);
 
 /**
- * Attach `selected` class to the the selected search result.
+ * Attach `selected` class to the the selected autocomplete result.
  */
 function handleSearchCursorUpDown(down) {
-  const sel = sr.querySelector(`.selected`);
+  const sel = ac_results.querySelector(`.selected`);
   if (sel) {
     sel.classList.remove("selected");
     const toSelect = down
-      ? sel.nextSibling || sr.firstChild
-      : sel.previousSibling || sr.lastChild;
+      ? sel.nextSibling || ac_results.firstChild
+      : sel.previousSibling || ac_results.lastChild;
     toSelect && toSelect.classList.add("selected");
   } else {
-    const toSelect = down ? sr.firstChild : sr.lastChild;
+    const toSelect = down ? ac_results.firstChild : ac_results.lastChild;
     toSelect && toSelect.classList.add("selected");
   }
 }
@@ -33,12 +42,12 @@ function handleSearchCursorUpDown(down) {
  * Perform search (when enter is pressed).
  */
 function handleSearchEnter() {
-  const sel = sr.querySelector(`.selected`) || sr.firstChild;
+  const sel = ac_results.querySelector(`.selected`) || ac_results.firstChild;
   sel.click();
 }
 
 /**
- * Allow user to navigate search results with up/down arrow keys, and choose with enter.
+ * Allow user to navigate autocomplete results with up/down arrow keys, and choose with enter.
  */
 SEARCH_INPUT.addEventListener("keydown", (ev) => {
   switch (ev.key) {
@@ -71,7 +80,7 @@ function removeAllChildren(node) {
 /**
  * Handle user input and perform search.
  */
-function handleSearch(dataCenter, err, ev) {
+function handleSearch(dataCenter, err, ev, sr, maxResults) {
   const text = ev.target.value;
 
   // If no input clear all.
@@ -85,12 +94,12 @@ function handleSearch(dataCenter, err, ev) {
   sr.setAttribute("state", "loading");
 
   if (dataCenter) {
-    const result = dataCenter.search(text, false);
+    const result = dataCenter.search(text, false, maxResults);
 
     // in case user has updated the input.
     if (ev.target.value != text) return;
   
-    // update search results
+    // update autocomplete results
     removeAllChildren(sr);
     for (const { name, docLink } of result) {
       const d = sr.appendChild(document.createElement("a"));
@@ -111,8 +120,15 @@ function handleSearch(dataCenter, err, ev) {
 DeclarationDataCenter.init()
   .then((dataCenter) => {
     // Search autocompletion.
-    SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev));
+    SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, ac_results, AC_MAX_RESULTS));
+    if(SEARCH_PAGE_INPUT) {
+      SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS))
+      SEARCH_PAGE_INPUT.dispatchEvent(new Event("input"))
+    }
   })
   .catch(e => {
-    SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev));
+    SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS));
+    if(SEARCH_PAGE_INPUT) {
+      SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS));
+    }
   });
diff --git a/static/style.css b/static/style.css
index 2944e99..0701500 100644
--- a/static/style.css
+++ b/static/style.css
@@ -116,7 +116,7 @@ header {
     :root { --header-side-padding: 1ex; }
     #search_form button { display: none; }
     #search_form input { width: 100%; }
-    header #search_results {
+    header #autocomplete_results {
         left: 1ex;
         right: 1ex;
         width: inherit;
@@ -146,7 +146,7 @@ header header_filename {
 }
 
 /* inserted by nav.js */
-#search_results {
+#autocomplete_results {
     position: absolute;
     top: var(--header-height);
     right: calc(var(--header-side-padding));
@@ -160,15 +160,15 @@ header header_filename {
     max-height: calc(100vh - var(--header-height));
 }
 
-#search_results:empty {
+#autocomplete_results:empty {
     display: none;
 }
 
-#search_results[state="loading"]:empty {
+#autocomplete_results[state="loading"]:empty {
     display: block;
     cursor: progress;
 }
-#search_results[state="loading"]:empty::before {
+#autocomplete_results[state="loading"]:empty::before {
     display: block;
     content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 ';
     padding: 1ex;
@@ -179,17 +179,17 @@ header header_filename {
     100% { transform: translate(-100%, 0); }
 }
 
-#search_results[state="done"]:empty {
+#autocomplete_results[state="done"]:empty {
     display: block;
     text-align: center;
     padding: 1ex;
 }
-#search_results[state="done"]:empty::before {
+#autocomplete_results[state="done"]:empty::before {
     content: '(no results)';
     font-style: italic;
 }
 
-#search_results a {
+#autocomplete_results a {
     display: block;
     color: inherit;
     padding: 1ex;
@@ -197,11 +197,20 @@ header header_filename {
     padding-left: 0.5ex;
     cursor: pointer;
 }
-#search_results .selected {
+#autocomplete_results .selected {
     background: white;
     border-color: #f0a202;
 }
 
+#search_results a {
+    display: block;
+}
+
+#search_results[state="done"]:empty::before {
+    content: '(no results)';
+    font-style: italic;
+}
+
 main, nav {
     margin-top: calc(var(--header-height) + 1em);
 }
@@ -476,7 +485,7 @@ main h2, main h3, main h4, main h5, main h6 {
 }
 
 .imports li, code, .decl_header, .attributes, .structure_field_info,
-        .constructor, .instances li, .equation, #search_results div,
+        .constructor, .instances li, .equation, #autocomplete_results div,
         .structure_ext_ctor {
     font-family: 'Source Code Pro', monospace;
 }