add content to the home page

Author: RemyDegenne

home_page/_config.yml

@@ -20,15 +20,15 @@
 
 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:
 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
+  - jekyll-github-metadata

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/)
+* [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!