docs: Improve website docs

doc/_layouts/default.html

@@ -16,7 +16,7 @@
     <a id="skip-to-content" href="#content">Skip to the content.</a>
 
     <header class="page-header" role="banner">
-      <h1 class="project-name">{{ page.title | default: site.title | default: site.github.repository_name }}</h1>
+      <h1 class="project-name">{{ site.title | default: site.github.repository_name }}</h1>
       <h2 class="project-tagline">{{ page.description | default: site.description | default: site.github.project_tagline }}</h2>
       <a href="https://heplean.github.io/HepLean/docs/" class="btn">Documentation</a>
       {% if site.github.is_project_page %}

doc/assets/css/style.scss

@@ -10,3 +10,12 @@
 body {
   background-color: #E1DEC2;
 }
+
+.main-content h1,
+.main-content h2,
+.main-content h3,
+.main-content h4,
+.main-content h5,
+.main-content h6 {
+  color: #2F4456;
+}

doc/index.markdown

@@ -6,6 +6,57 @@
 # To view changes run: bundle exec jekyll serve
 #layout: home
 ---
+# Content 
+
+- [What is HepLean?](https://heplean.github.io/HepLean/#what-is-heplean)
+- [How to get involved?](https://heplean.github.io/HepLean/#how-to-get-involved)
+- [Coverage](https://heplean.github.io/HepLean/#coverage)
+
+# What is HepLean
+
+HepLean is an open-source project to digitalise definitions, theorems, proofs, and calculations in high energy physics using the interactive theorem prover Lean 4.
+
+HepLean has the potential to benefit the high energy physics community in four ways: 
+- Make it easier to find results. 
+- Make it easier to automate the creation of new results using e.g. machine learning methods. 
+- Make it easier to check papers and results for mathematical correctness. 
+- Create new avenues through which high energy physics can be taught. 
+
+HepLean is a connection between high energy physics (both formal and pheno), 
+computer science, and mathematics.
+# How to get involved? 
+
+There are a number of ways to get involved in HepLean. 
+
+- <b>Improve documentation</b>: If you have never worked on Lean before but have a background 
+in high-energy physics, a good place to start contributing is to improve documentation 
+on existing code in HepLean. If you need any pointers, please get in touch. 
+- <b>Golfing and improving proofs</b>: Many of the proofs in HepLean are not as concise, 
+or as short as they could be. Golfing (making shorter) existing proofs is useful benefit 
+to HepLean. 
+- <b>Improving current areas</b>: There are a number of areas of high energy physics currently in HepLean.
+ These are by no means complete, and we would love to see new lemmas, theorems and 
+definitions added.  
+- <b>Add a new area</b>: We want HepLean to expand into a new areas of high energy physics. 
+If you have expertise in any area and would like to see it digitalised, either get in touch or 
+make a relavent pull-request on GitHub. 
+- <b>Develop new tactics</b>: A benifit of Lean is the ability to automate proofs. This 
+is often done through proof tactics. The development of such tactics specific to high-energy physics 
+will make it easier for the high-energy physics to use and adapt to Lean. 
+- <b>Coding aspects</b>: Improvements to GitHub workflows, and other structural aspects of this
+project are greatly appreciated. 
+
+# Coverage 
+
+Any area not appearing in the below table has zero coverage in HepLean. 
+
+| Area | Low Coverage | Medium | High | How to Help? |
+| --- | --- | --- | --- | --- |
+| [Anomaly cancellation](https://heplean.github.io/HepLean/docs/HepLean/AnomalyCancellation/Basic.html)| ✔️ | ✔️ | ✔️ | Docs, golf |
+| [CKM Matrix](https://heplean.github.io/HepLean/docs/HepLean/FlavorPhysics/CKMMatrix/Basic.html) | ✔️ | ✔️ | ✔️ | Docs, golf |
+| [Higgs potential](https://heplean.github.io/HepLean/docs/HepLean/StandardModel/HiggsBoson/Basic.html) | ✔️ |  ✘ |  ✘ | Docs, golf, new lemmas etc. |
+| [Feynman diagrams](https://heplean.github.io/HepLean/docs/HepLean/FeynmanDiagrams/Basic.html) | ✔️ | ✘  | ✘  |  |
+| [Lorentz Group](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html) | ✔️ | ✘  | ✘  | New lemmas etc.|
+| [2HDM](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html) | ✔️ | ✘  | ✘  | New lemmas etc. |
+
 
-(This site is a work in progress. More to follow. Follow the links above to 
-the documentation page or GitHub.)