An Attempt to formalize physics in Lean4.

Find a file

jstoobysmith 10486f3a58 refactor: Lint		2024-04-18 10:50:59 -04:00
.github/workflows	Updated docs	2024-04-17 08:48:09 -04:00
.lake	lakefiles	2024-04-17 09:20:51 -04:00
HepLean/AnomalyCancellation	refactor: Lint	2024-04-18 10:50:59 -04:00
scripts	feat: Add relation to mathlib4 defns	2024-04-17 10:25:05 -04:00
.DS_Store	Initial	2024-04-16 15:31:25 -04:00
.gitignore	Update gitignore	2024-04-17 08:38:00 -04:00
HepLean.lean	feat: Add low dim U(1)	2024-04-18 10:50:21 -04:00
lake-manifest.json	feat: Add results relating to the SM ACCs	2024-04-17 14:25:17 -04:00
lakefile.lean	Update lakefile.lean	2024-04-17 08:02:26 -04:00
lean-toolchain	Initial	2024-04-16 15:31:25 -04:00
README.md	Updated docs	2024-04-17 08:48:09 -04:00

README.md

High Energy Physics in Lean

Aim of this project:

Use Lean to create a database of definitions, theorems and proofs in high energy physics.
Keep the database up-to date with developments in MathLib4.
Create github workflows of relevence to the high energy physics community.

The documentation for this project can be found at:

https://heplean.github.io/HepLean/

To learn more about this project see:

https://leanprover.zulipchat.com/#narrow/stream/395462-Natural-sciences/topic/Anomaly.20cancellation.20conditions

Contributing

We follow here the same contribution policies as MathLib4. If you want permission to create a pull-request for this repository contact Joseph Tooby-Smith on the lean Zulip, or email.

Installation

Installing Lean 4

See: https://leanprover-community.github.io/get_started.html

Quick installation

Clone this repository.
Open a terminal in the cloned directory.
Run lake -Kenv=dev update.

Depending on how up to date this directory is compared to MathLib4 this may lead to errors.