DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #326 from HEPLean/WickTheoremDoc

Browse source 
feat: Website include code snippet
This commit is contained in:
Joseph Tooby-Smith 2025-02-10 15:49:33 +00:00 • committed by GitHub
commit 9d302c9a47
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

BIN
docs/assets/WicksTheoremScreenShot.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 82 KiB

14
docs/index.markdown
View file

@ -7,10 +7,24 @@
#layout: home
---
<div class="example-container" style="border: 2px solid #ddd; border-radius: 8px; padding: 20px; margin: 20px 0; box-shadow: 0 2px 4px rgba(0,0,0,0.1);">
<div style="text-align: center;">
<img src="/assets/WicksTheoremScreenShot.png"
alt="Screenshot of Wick's theorem implementation in HepLean"
style="width: 100%; height: auto; border-radius: 4px;">
<p style="margin-top: 10px; font-style: italic; color: #666;">
The above screenshot demonstrates how theorems are formalized in HepLean.
</p>
</div>
</div>
# 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.