diff --git a/templates/_base.html b/templates/_base.html
index 5c70fc6a0e..0990523531 100644
--- a/templates/_base.html
+++ b/templates/_base.html
@@ -7,6 +7,7 @@
 
   <link rel="stylesheet" href="{{base_url}}/css/lean.css" >
   <link rel="shortcut icon" href="{{base_url}}/img/favicon.ico">
+  <link rel="search" type="application/opensearchdescription+xml" title="mathlib docs" href="{{base_url}}/opensearch.xml">
 <link href="https://fonts.googleapis.com/css2?family=Merriweather&family=Open+Sans&family=Source+Code+Pro:wght@400;600&display=swap" rel="stylesheet">
     {% block extracss %}{% endblock %}
 
diff --git a/templates/opensearch.xml b/templates/opensearch.xml
new file mode 100644
index 0000000000..9d2702dbe2
--- /dev/null
+++ b/templates/opensearch.xml
@@ -0,0 +1,8 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<OpenSearchDescription xmlns="http://a9.com/-/spec/opensearch/1.1/" xmlns:moz="http://www.mozilla.org/2006/browser/search/">
+  <ShortName>mathlib</ShortName>
+  <Description>Search mathlib docs</Description>
+  <InputEncoding>UTF-8</InputEncoding>
+  <Image width="16" height="16" type="image/x-icon">{{base_url}}/img/favicon.ico</Image>
+  <Url type="text/html" method="GET" template="{{base_url}}/mathlib_docs/find/{searchTerms}" />
+</OpenSearchDescription>