diff --git a/docs/assets/WicksTheoremScreenShot.png b/docs/assets/WicksTheoremScreenShot.png new file mode 100644 index 0000000..1818f1f Binary files /dev/null and b/docs/assets/WicksTheoremScreenShot.png differ diff --git a/docs/index.markdown b/docs/index.markdown index e8509dc..ada618f 100644 --- a/docs/index.markdown +++ b/docs/index.markdown @@ -7,10 +7,24 @@ #layout: home --- + + +
+
+ Screenshot of Wick's theorem implementation in HepLean +

+ The above screenshot demonstrates how theorems are formalized in HepLean. +

+
+
+ # 1. Mission of HepLean The mission of HepLean is to digitalize results, meaning definitions, theorems and calculations, from physics into Lean 4 with an initial focus on high energy physics and in a way which is useful to the broad physics community. + # 2. Vision of HepLean **Statement**: HepLean aspires to be the definitive formal repository for physics in Lean, akin to Mathlib for mathematics, with both the Lean and physics communities behind it and a potential formal collaboration.