PhysLean is a Lean 4 formalization library for mainstream physics. The project digitalizes physics results (definitions, theorems, calculations) from domains including classical mechanics, quantum mechanics, statistical mechanics, electromagnetism, relativity, quantum field theory, and particle physics. The codebase is organized by physics domain rather than mathematical structure, with comprehensive documentation requirements for each module.
This page provides a high-level overview of the project's architecture, major components, and development workflow. For installation and build instructions, see Getting Started. For details on the mathematical infrastructure, see Core Mathematical Framework. For specific physics domains, see Physics Domains.
PhysLean follows a three-layer architecture: physics formalizations at the top, mathematical foundations in the middle, and development infrastructure at the bottom.
Sources: PhysLean.lean1-393 README.md1-136 lakefile.toml1-158
The root module PhysLean.lean1-393 imports all major physics and mathematics modules. The project uses Lean 4 version 4.26.0 (lean-toolchain1) with mathlib v4.26.0 as its primary dependency (lakefile.toml11-14).
| Component | File/Module | Purpose |
|---|---|---|
| Root module | PhysLean.lean | Aggregates all physics and math imports |
| Build config | lakefile.toml | Lake build system configuration |
| Dependencies | lake-manifest.json | Locked dependency versions |
| Toolchain | lean-toolchain | Specifies Lean version (v4.26.0) |
Sources: PhysLean.lean1-393 lakefile.toml1-158 lake-manifest.json1-136 lean-toolchain1
PhysLean formalizes seven major physics domains. Each domain consists of multiple modules organized hierarchically.
Sources: PhysLean.lean1-17 PhysLean.lean76-92 PhysLean.lean228-247 PhysLean.lean357-361
The table below lists the main structures defined in each physics domain:
| Domain | Key Structure | File | Description |
|---|---|---|---|
| Classical Mechanics | HarmonicOscillator | PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean100-106 | Mass-spring system with m and k |
| Classical Mechanics | InitialConditions | PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean82-86 | Position x₀ and velocity v₀ |
| Quantum Mechanics | HilbertSpace | PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean | L² functions on ℝ |
| Statistical Mechanics | CanonicalEnsemble | PhysLean/StatisticalMechanics/CanonicalEnsemble/Basic.lean | Partition function framework |
| QFT | FieldSpecification | PhysLean/QFT/PerturbationTheory/FieldSpecification/Basic.lean | Field operators and statistics |
| QFT | WickContraction | PhysLean/QFT/PerturbationTheory/WickContraction/Basic.lean | Pairings for Wick's theorem |
Sources: PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean100-106 PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean82-86
The classical harmonic oscillator demonstrates the project's approach. The structure HarmonicOscillator is defined with fields m (mass) and k (spring constant) with positivity constraints (PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean100-106). The module proves:
EquationOfMotion: Euler-Lagrange equations (PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean462-463)equationOfMotion_iff_newtons_2nd_law: Equivalence to Newton's second law (PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean563-566)energy_conservation_of_equationOfMotion: Energy conservation (PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean593-595)trajectory_equationOfMotion: Solutions satisfy equations of motion (PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean403-420)Sources: PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean100-106 PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean403-420
The mathematics layer provides reusable abstractions for physics formalizations. The core types are Space d, Time, and SpaceTime d, along with generic tensor and distribution frameworks.
Sources: PhysLean/SpaceAndTime/Space/Basic.lean38-41 PhysLean/SpaceAndTime/Time/Basic.lean72-74
The fundamental geometric types are:
Space d (PhysLean/SpaceAndTime/Space/Basic.lean38-41): A structure wrapping Fin d → ℝ, representing d-dimensional Euclidean space. It has instances for:
InnerProductSpace ℝ (Space d) (PhysLean/SpaceAndTime/Space/Basic.lean353-376)FiniteDimensional ℝ (Space d) (PhysLean/SpaceAndTime/Space/Basic.lean493-494)MeasurableSpace (Space d) (PhysLean/SpaceAndTime/Space/Basic.lean384)basis : OrthonormalBasis (Fin d) ℝ (Space d) (PhysLean/SpaceAndTime/Space/Basic.lean434-452)Time (PhysLean/SpaceAndTime/Time/Basic.lean72-74): A structure wrapping ℝ, representing time with arbitrary units and origin. It has:
InnerProductSpace ℝ Time (PhysLean/SpaceAndTime/Time/Basic.lean321-325)Module.finrank ℝ Time = 1 (PhysLean/SpaceAndTime/Time/Basic.lean405-413)basis : OrthonormalBasis (Fin 1) ℝ Time (PhysLean/SpaceAndTime/Time/Basic.lean354-384)SpaceTime d: Defined as an alias for Lorentz.Vector d in the Relativity modules, representing (d+1)-dimensional Minkowski spacetime.
Sources: PhysLean/SpaceAndTime/Space/Basic.lean38-41 PhysLean/SpaceAndTime/Time/Basic.lean72-74
The tensor framework uses a generic TensorSpecies structure that is specialized for physics:
TensorSpecies k C G (PhysLean/Relativity/Tensors/TensorSpecies/Basic.lean): Generic tensor definition with ComponentIdx and basisLorentz.Vector and Lorentz.CoVector: Real tensors for Lorentz transformationsTensorial typeclass (PhysLean/Relativity/Tensors/Tensorial.lean): Interface for tensor-like typesThe tensor framework enables index notation and contraction operations used throughout electromagnetism, relativity, and QFT modules.
Sources: PhysLean.lean275-328
Distribution (PhysLean/Mathematics/Distribution/Basic.lean49): Type alias for 𝓢(E,𝕜) →L[𝕜] F, representing tempered distributions. Used for:
Variational Calculus modules define:
HasVarAdjoint (PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean): Adjoint with respect to inner productHasVarAdjDerivAt (PhysLean/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean): Variational adjoint derivativesHasVarGradient (PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean): Variational gradients for functionalsThese are used to formulate Euler-Lagrange equations in classical mechanics (PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean433-436).
Sources: PhysLean/Mathematics/Distribution/Basic.lean PhysLean/Mathematics/VariationalCalculus/Basic.lean
PhysLean includes extensive tooling for code quality, documentation generation, and project management.
lakefile.toml (lakefile.toml1-158) configures:
Sources: lakefile.toml1-158 lake-manifest.json1-136
PhysLean enforces code quality through multiple linting layers:
| Linter | File | Purpose |
|---|---|---|
lint_all | lakefile.toml41-43 | Orchestrates all linters |
style_lint | lakefile.toml33-34 | Text-based style checks |
sorry_lint | lakefile.toml51-53 | Tracks @sorryful and @pseudo axioms |
runPhysLeanLinters | lakefile.toml56-58 | Batteries linter integration |
module_doc_lint | lakefile.toml81-82 | Validates module documentation structure |
redundant_imports | lakefile.toml76-78 | Detects transitive imports |
check_dup_tags | lakefile.toml46-48 | Ensures TODO tag uniqueness |
The linters enforce:
sorryAx must have @sorryful)Sources: lakefile.toml28-82 scripts/MetaPrograms/module_doc_lint.lean1-311
Documentation is generated through:
doc-gen4 generates API reference from source code (lakefile.toml16-19)find_TODOs.lean scans for /-! TODO: tag ... -/ comments (lakefile.toml116-117)notes.lean generates structured physics notes (lakefile.toml120-122)The module_doc_lint enforces an 8-step documentation structure for each module:
# ## i. Overview## ii. Key results## iii. Table of contents## iv. References## A., ### A.1.)Sources: lakefile.toml98-122 scripts/MetaPrograms/module_doc_lint.lean28-207
PhysLean.Meta.Basic (PhysLean.lean76) provides utilities for code introspection:
allImports: Enumerate all importsgetUserConsts: Extract user-defined constantsEnvironment Extensions:
sorryfulExtension: Tracks declarations marked @sorryfulpseudoExtension: Tracks declarations marked @pseudoThese extensions enable bidirectional contract enforcement between attributes and axiom usage.
Sources: PhysLean.lean75-89
Every PhysLean module must include structured documentation following this format:
The module_doc_lint script (scripts/MetaPrograms/module_doc_lint.lean70-207) validates this structure, checking:
#, ##, ###, ####)## A., ### A.1., #### A.1.1.)Files exempt from linting are listed in scripts/MetaPrograms/module_doc_no_lint.txt1-321
Sources: scripts/MetaPrograms/module_doc_lint.lean1-311 scripts/MetaPrograms/module_doc_no_lint.txt1-321
PhysLean uses GitHub Actions for CI/CD (README.md27):
The CI pipeline runs in parallel jobs validating different aspects:
Sources: README.md1-136
Based on the README and importance scores:
The project is completely open-source, community-run, and independent (README.md46-47), with emphasis on mainstream physics only (README.md50).
Sources: README.md1-136 lean-toolchain1 lakefile.toml1-158
For detailed information on specific topics:
For contributing guidelines and TODO items, see the project website and Zulip channel referenced in README.md16-17
Sources: README.md1-136
Refresh this wiki
This wiki was recently refreshed. Please wait 7 days to refresh again.