From cd628ee3eeadd6c578b80cbba172e58e8764e9f7 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 19 Jan 2026 09:07:59 +0100 Subject: [PATCH] add content to the home page --- home_page/_config.yml | 6 +++--- home_page/index.md | 12 +++++++----- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/home_page/_config.yml b/home_page/_config.yml index 030199ee..114d6db8 100644 --- a/home_page/_config.yml +++ b/home_page/_config.yml @@ -20,7 +20,7 @@ title: LeanBandits #email: your-email@example.com -description: by Remy Degenne +description: A Lean formalization of bandit algorithms by Remy Degenne and Paulo Rauber baseurl: "" # the subpath of your site, e.g. /blog url: "https://RemyDegenne.github.io/lean-bandits" # the base hostname & protocol for your site, e.g. http://example.com twitter_username: @@ -28,7 +28,7 @@ github_username: RemyDegenne repository: RemyDegenne/lean-bandits # Build settings -remote_theme: pages-themes/cayman@v0.2.0 +remote_theme: pages-themes/cayman@v0.2.0 plugins: - jekyll-remote-theme - - jekyll-github-metadata \ No newline at end of file + - jekyll-github-metadata diff --git a/home_page/index.md b/home_page/index.md index 2ab3ac6f..92473907 100644 --- a/home_page/index.md +++ b/home_page/index.md @@ -6,10 +6,12 @@ usemathjax: true --- +Bandit algorithms and proofs of their regret bounds, in Lean. + Useful links: -* [Zulip chat for Lean](https://leanprover.zulipchat.com/) for coordination -* [Blueprint]({{ site.url }}/blueprint/) -* [Blueprint as pdf]({{ site.url }}/blueprint.pdf) -* [Dependency graph]({{ site.url }}/blueprint/dep_graph_document.html) -* [Doc pages for this repository]({{ site.url }}/docs/) \ No newline at end of file +* [Blueprint]({{ site.url }}/blueprint/): a latex document describing the content of the repository, served as html, with links to the code. +* [Blueprint as pdf]({{ site.url }}/blueprint.pdf): the same document as a pdf +* [Dependency graph]({{ site.url }}/blueprint/dep_graph_document.html): a graph of all definitions and theorems in the project, showing their dependencies +* [Doc pages for this repository]({{ site.url }}/docs/): documentation of every declaration in the Lean code. +* [Zulip chat for Lean](https://leanprover.zulipchat.com/): the Lean community chat room. Ask any general Lean or Mathlib question there!