Getting Started in PhysLean

This is a guide for getting started with PhysLean, aimed at people with no Lean experience or who are new to the project.

Useful resources

🎮 The Natural Numbers Game 📺 Lean for Scientists and Engineers Lectures by Tyler Josephson

Installing

Lean Installation Guide

Ready to get started with Lean? Click the button below to see the installation instructions:

Install Lean

PhysLean Installation Steps

Follow these steps to install PhysLean:

Clone the repository: https://github.com/HEPLean/PhysLean
Run the following commands in the top-level PhysLean directory:

lake update 
lake exe cache get
lake build

Here lake build may take around 20 minutes.

Trouble-shooting

Sometimes things go wrong due to no fault of your own. PhysLean or one of its dependencies may have been updated to a new version of Lean for example. In these cases you can try the following:

rm -rf .lake
lake update
lake exe cache get
lake build

or as a single command:

rm -rf .lake; lake update; lake exe cache get; lake build

Writing results

Things to bear in mind:

It helps if results sit next to results about the same physics.
Informal results and semi-formal results are easier to write if you're new to Lean.
If you make (somewhat substantial) changes to a file, feel free to add your self to the author list, in alphabetic order by last-name.

Definitions

Definitions are used to introduce new concepts or objects in a precise and formal way. In PhysLean we give all definitions doc-strings.

        
/-- For a harmonic oscillator, the Schrodinger Operator corresponding to it
is defined as the function from `ℝ → ℂ` to `ℝ → ℂ` taking

`ψ ↦ - ℏ^2 / (2 * m) * ψ'' + 1/2 * m * ω^2 * x^2 * ψ`. -/
noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
    fun x => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) x) + 1/2 * Q.m * Q.ω^2 * x^2 * ψ x

structure, inductive and abbrev also introduce new concepts in a similar way to def.

Lemmas

In PhysLean we use lemmas for every theorem which is not a main one. For every lemma you must provide a proof e.g.

        
lemma schrodingerOperator_parity (ψ : ℝ → ℂ) :
    Q.schrodingerOperator (parity ψ) = parity (Q.schrodingerOperator ψ) := by
    funext x
    have (ψ : ℝ → ℂ) : (fun x => (deriv fun x => ψ (-x)) x) = fun x => - deriv ψ (-x) := by
    funext x
    rw [← deriv_comp_neg]
    simp [schrodingerOperator, parity, this]

Theorems

Theorems are significant results, but are otherwise exactly the same as lemmas.

        
theorem wicks_theorem_normal_order : (φs : List 𝓕.FieldOp) →
    𝓣(𝓝(ofFieldOpList φs)) =
    ∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), φsΛ.1.wickTerm := by 
  ...

Informal Definitions

Informal definitions are definitions written in English rather than in Lean. They are given a tag (you can get a tag using lake exe make_tag), and a list of dependencies. The definition itself is written in the doc-string. They can not be used in further results.

        
/-- The hubble constant defined in terms of the scale factor
as `(dₜ a) / a`.

The notation `H` is used for the `hubbleConstant`. -/
informal_definition hubbleConstant where
    deps := []
    tag := "6Z2NB"

Informal Lemmas

Informal lemmas are lemmas written in English rather than in Lean. They are given a tag (you can get a tag using lake exe make_tag), and a list of dependencies. The lemma and proof itself are written in the doc-string. They can not be used in further results.

        
/-- The time evolution of the hubble parameter is equal to `dₜ H = - H^2 (1 + q)`. -/
informal_lemma time_evolution_hubbleConstant where
    deps := [hubbleConstant]
    tag := "6Z3BS"

Semi-Formal Results

Semi-formal results are like informal definitions and lemmas except the type of the definition or statement of the lemma is made formal. They are half-way between informal definitions and lemmas and formal statements. They cannot be used in further results. They are also given a tag.

        
/-- The force on the classical harmonic oscillator is `- k x`. -/
semiformal_result "6YB2U" force_is_linear (x : ℝ → ℝ) :
    force S x = - S.k • x

TODO items

Todo items are used to indicate things which are to be done. The consist of a tag and a string statement of what is to be done.

        
TODO "6VZHC" "Create a new folder for the damped harmonic oscillator, initially as a place-holder."

Making a new file

When to make a new file?

New files should be made when there is a natural seperation of results in an existing file. Or when a new result is being added to the project which does not fit in any existing file.

Making a New File

Create a new file: Place the file in the relevant directory.
File naming convention: Use a descriptive name with only alphabetic characters. Each new word should start with a capital letter. For example: MyNewFile.lean.

Add a copyright statement: At the very top of the file, include the following:


/-
Copyright (c) 2025 your-name. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: your-name
-/

Replace your-name with your actual name.

Include necessary imports: Add any required imports next. For example:


import Mathlib.Analysis.SpecialFunctions.Integrals
import Mathlib.Analysis.SpecialFunctions.PolarCoord
import PhysLean.Meta.TODO.Basic
import PhysLean.Meta.Informal.SemiFormal
import PhysLean.Meta.Informal.Basic

Add a file description: Provide a brief description of the file's content. For an example of a good description, see this file.
Update the main import file: Add your new file to ./PhysLean.lean in alphabetical order as an import.

Linting

What is Linting?

Linting is the process of checking your code for potential errors, stylistic issues, and adherence to coding standards. It helps ensure that your code is clean, consistent, and free from common mistakes.

On making a pull-request to PhysLean, GitHub workflows will lint your code automatically.

Linting Locally

You can also check your code locally using the following commands:

lake exe lint_all
./scripts/lint-style.sh

Ensuring these commands do not bring up errors helps maintain the quality of PhysLean!

Making a pull-request

Things to bear in mind:

Small pull-requests are better the large ones - even if it's just a single result.

Using Forks

Fork the PhysLean repository to your GitHub account.

Clone your forked repository to your local machine.

Make your changes on your local version.

Push your changes to your forked repository.

Open a pull request from your forked version to the main PhysLean repository.

Using Branches

Ask Joseph Tooby-Smith to add you as an outside collaborator on the project.
Clone the main GitHub repository.
Make your own branch (calling it something like feat(your-name):updating spacetime is helpful).
Open a pull request from your branch to the main branch.

PhysLean: Digitalizing Physics in Lean 4

An open-source, community, project to digitalize results from physics into Lean 4.

Getting Started in PhysLean

Table of Contents

📚 Getting Started

✍️ Writing & Development

🔧 Code Quality & Contribution

Useful resources

Installing

Lean Installation Guide

PhysLean Installation Steps

Trouble-shooting

Writing results

Things to bear in mind:

Definitions

Lemmas

Theorems

Informal Definitions

Informal Lemmas

Semi-Formal Results

TODO items

Making a new file

When to make a new file?

Making a New File

Linting

What is Linting?

Linting Locally

Making a pull-request

Things to bear in mind:

Using Forks

Using Branches