From 3111f4c15f200534e2fbfbd1a0d8ac6f1a49704d Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sun, 12 Apr 2026 15:05:01 +0200
Subject: [PATCH 1/2] fix some website errors

---
 website/Main.lean           |  8 +-------
 website/Site/FrontPage.lean | 18 +++++++++---------
 2 files changed, 10 insertions(+), 16 deletions(-)

diff --git a/website/Main.lean b/website/Main.lean
index 7f04b669..e3159288 100644
--- a/website/Main.lean
+++ b/website/Main.lean
@@ -22,18 +22,12 @@ def theme : Theme := { Theme.default with
             r!"document.addEventListener('DOMContentLoaded', () => { const lightbox = GLightbox(); });"
           </script>
           {{← builtinHeader }}
-        <!-- Privacy-friendly analytics by Plausible -->
-        <script async src="https://plausible.io/js/pa--0OdxwGCKX8nhJ0vma6XG.js"></script>
-        <script>
-          "window.plausible=window.plausible||function(){(plausible.q=plausible.q||[]).push(arguments)},plausible.init=plausible.init||function(i){plausible.o=i||{}};
-          plausible.init()"
-        </script>
         </head>
         <body>
           <header>
             <nav class="navbar">
               <div class="nav-inner">
-                <a class="logo" href="/">"Lean Machine Learning"</a>
+                <a class="logo" href>"Lean Machine Learning"</a>
                 <div class="nav-links">
                   <a href="#goals">"Goals"</a>
                   <a href="#get-started">"Get Started"</a>
diff --git a/website/Site/FrontPage.lean b/website/Site/FrontPage.lean
index 0e6ed2fd..40ee860a 100644
--- a/website/Site/FrontPage.lean
+++ b/website/Site/FrontPage.lean
@@ -18,19 +18,19 @@ The Lean library for machine learning research
 Lean Machine Learning is a carefully curated library of formalized definitions and theorems in machine learning theory, verified in [Lean](https://lean-lang.org). It provides a trusted foundation for researchers to explore and formalize machine learning algorithms with mathematical rigor.
 
 ::::html a (class := "hero-btn primary") (href := "https://github.com/remydegenne/lean-bandits")
-:::html img (src := "/static/arrow.svg") (alt := "") (width := "20") (height := "20")
+:::html img (src := "/lean-bandits/static/arrow.svg") (alt := "") (width := "20") (height := "20")
 :::
 Get Started
 ::::
 
 ::::html a (class := "hero-btn secondary") (href := "tutorial")
-:::html img (src := "/static/book.svg") (alt := "") (width := "20") (height := "20")
+:::html img (src := "/lean-bandits/static/book.svg") (alt := "") (width := "20") (height := "20")
 :::
 Tutorials
 ::::
 
 ::::html a (class := "hero-btn secondary") (href := "docs")
-:::html img (src := "/static/book.svg") (alt := "") (width := "20") (height := "20")
+:::html img (src := "/lean-bandits/static/book.svg") (alt := "") (width := "20") (height := "20")
 :::
 Documentation
 ::::
@@ -141,31 +141,31 @@ Learn more about Lean Machine Learning with the tutorials and documentation, or
 :::::htmlDiv (class := "cta-buttons")
 
 ::::html a (class := "cta-btn primary") (href := "https://github.com/remydegenne/lean-bandits")
-:::html img (src := "/static/arrow.svg") (alt := "") (width := "20") (height := "20")
+:::html img (src := "/lean-bandits/static/arrow.svg") (alt := "") (width := "20") (height := "20")
 :::
 View on GitHub
 ::::
 
 ::::html a (class := "cta-btn secondary") (href := "tutorial")
-:::html img (src := "/static/book.svg") (alt := "") (width := "20") (height := "20")
+:::html img (src := "/lean-bandits/static/book.svg") (alt := "") (width := "20") (height := "20")
 :::
 Tutorials
 ::::
 
 ::::html a (class := "cta-btn secondary") (href := "docs")
-:::html img (src := "/static/book.svg") (alt := "") (width := "20") (height := "20")
+:::html img (src := "/lean-bandits/static/book.svg") (alt := "") (width := "20") (height := "20")
 :::
 Documentation
 ::::
 
 ::::html a (class := "cta-btn secondary") (href := "roadmap")
-:::html img (src := "/static/book.svg") (alt := "") (width := "20") (height := "20")
+:::html img (src := "/lean-bandits/static/book.svg") (alt := "") (width := "20") (height := "20")
 :::
 Roadmap
 ::::
 
 ::::html a (class := "cta-btn secondary") (href := "https://leanprover.zulipchat.com/")
-:::html img (src := "/static/zulip.svg") (alt := "") (width := "20") (height := "20")
+:::html img (src := "/lean-bandits/static/zulip.svg") (alt := "") (width := "20") (height := "20")
 :::
 Join Zulip
 ::::
@@ -184,7 +184,7 @@ We are grateful for the support of the following organizations.
 
 :::::htmlDiv (class := "sponsor-card")
 ::::html a (href := "https://www.inria.fr/")
-:::html img (src := "/static/Inria_logo_RGB.png") (alt := "Inria")
+:::html img (src := "/lean-bandits/static/Inria_logo_RGB.png") (alt := "Inria")
 :::
 ::::
 Inria FORMAL exploratory action

From 5557b4ae0376cd198119228a499b12ce5c7c0e65 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sun, 12 Apr 2026 15:08:17 +0200
Subject: [PATCH 2/2] minor

---
 website/Main.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/website/Main.lean b/website/Main.lean
index e3159288..7dc67dd2 100644
--- a/website/Main.lean
+++ b/website/Main.lean
@@ -13,7 +13,7 @@ def theme : Theme := { Theme.default with
         <head>
           <meta charset="utf-8"/>
           <meta name="viewport" content="width=device-width, initial-scale=1"/>
-          <title>"Lean Machine Learning — Formalized ML Theory"</title>
+          <title>"Lean Machine Learning"</title>
           <link rel="icon" type="image/svg+xml" href="/lean-bandits/static/favicon.svg"/>
           <link rel="stylesheet" href="/lean-bandits/static/style.css"/>
           <link rel="stylesheet" href= "/lean-bandits/static/glightbox/css/glightbox.min.css"/>