Lean for Statistical Physics Checking

[casualphysicsenjoyer]

Can I use Lean to check the statistical physics I'm doing?

This is a talk I prepared for an Independent Science Society session today. Thank you to those who attended!

I've been trying to learn mathematical and chemical theory for biological applications. And despite being trained as a mathematician, the math I come across is pretty hard. So far it's been a mix of Markov chains and statistical field theory, which can be fiddly and counterintuitive. And like all hard math, it very easy to make mistakes without realising it, especially if you are relying at all on AI to guide you.

Doing math is a dangerous activity. If you are not careful, you might be wasting your time getting things wrong, because it's super easy to fool yourself. Everyone who has taken an analysis course knows that things that appear obvious in math might actually be super subtle. Mistakes in proofs happen to professional mathematicians all the time. And so the difficulty of getting things correct is a very real problem - in fact it's probably the problem.

And this problem is made a lot worse if you are working as an independent scientist.

But it's not just independent scientists who need to find ways to ensure correctness. Because most of the cool problems out there are interdisciplinary, it means that we now have incentive to figure out ways for non-math people to do correct math more efficiently. It is likely that undiscovered math in edge fields like statistical field theory for bio is just as hard as the established fields in physics. For example, in the Smith and Morowitz book on the origin and nature of life on Earth, there's quite a lot of statistical physics that I need to check. It is likely that there are mistakes on my end and also in the book, since math is hard.

And so I wanted to figure out a way to check my math work as rigorously as I can whilst I'm working, almost like a scratchpad, and I found that using Mathlib and Lean4 was good for this.

Here's how it works, and I'll also give a little starter pack.

So in Lean 4, you have types, and types form the core of what the language is about. If you have coded at all, for example, in C++, you know that you have to assign types to variables. We have the same concepts of these standard types in Lean. For example, they could be natural numbers, integers, booleans, or floats.

Code: Select all

-- The type comes after the colon.
def n : Nat  := 7        -- a natural number
def k : Int  := -3       -- an integer
def b : Bool := true     -- a boolean
def x : Float := 2.5     -- a floating-point number

-- #check reports the type of an expression.
#check n        -- n : Nat
#check b        -- b : Bool
#check (1 : Int) + 4    -- ... : Int

So what interesting things can we do with types? Well, one obvious way is to build a composite type out of basic types. So, for example, we could cross two types to make products, to make something like:

Code: Select all

Nat × Nat
Nat × Bool
Nat × Bool × Bool

For example, an element in Nat × Nat would be (1, 2), an element in Nat × Bool could be (2, true), or Nat × Bool × Bool could be (1, true, false).

Code: Select all

def p : Nat × Nat        := (1, 2)
def q : Nat × Bool       := (2, true)
def r : Nat × Bool × Bool := (1, true, false)

Lean is a language that will show the type once you check it.

Code: Select all

#check p        -- p : Nat × Nat
#check q        -- q : Nat × Bool
#check r        -- r : Nat × Bool × Bool

-- You can also check an anonymous value directly.
#check (2, true)            -- (2, true) : Nat × Bool
#check (1, true, false)     -- (1, true, false) : Nat × Bool × Bool

So there's a lot of things we can do with types, but types are much more flexible than you think as a structure for doing things. For example, we can also define a composite operation between two types, which is a mapping, and call this a type itself. For example, we could define the type Nat → Nat:

Code: Select all

-- A function from Nat to Nat.
def double : Nat → Nat := fun m => 2 * m

#check double        -- double : Nat → Nat

-- The mapping Nat → Nat is itself a type.
#check (Nat → Nat)   -- Nat → Nat : Type

Let's pick apart what the definition means in line 54. We define the 'double' function, and the colon means that it's of a particular type, which in this case is a mapping from Nat to Nat. And then the colon equals defines the instance of what this thing actually is, which is a member of that type.

Even multivariable functions can be written as compositions of types. So, for example, take the function that sends x and y to x + y. On the surface, this would look like the function Nat × Nat → Nat, but it could also be interpreted as Nat → Nat → Nat. Because the function takes the first element x and then creates a new function, which is defined as adding x to y.

Code: Select all

-- A two-argument function is really a function that returns a function.
def add : Nat → Nat → Nat := fun x => fun y => x + y

#check add        -- add : Nat → Nat → Nat

-- Applying one argument yields a new function.
#check add 3      -- add 3 : Nat → Nat
#check add 3 4    -- add 3 4 : Nat

Code: Select all

-- The same type, with the implied parentheses written out.
def add : Nat → (Nat → Nat) := fun x => fun y => x + y

The last two brackets are implied in Lean.

Now here's the kicker. The whole point of LEAN4 is that it's meant to be a language that helps us prove things. In logic, propositions are statements that are true or false, and these are known to be true or false based on proofs.

And so naturally, propositions are also a type in lean.

Code: Select all

-- `True` is a proposition: its type is Prop.
#check True            -- True : Prop

And just as before, we can also define composite types on propositions. For example, we could make an 'and' proposition which looks like the following

Code: Select all

-- Given two propositions p and q, their conjunction p ∧ q is itself a proposition.
variable (p q : Prop)

#check p ∧ q          -- p ∧ q : Prop

Ok, so what are proofs? Well, proofs are a definition of a proposition. This means that just as we can define 7 as a term of Nat, a proof is a valid term of a Prop. This means that to find a proof of a proposition p, the game is to conjure up a term that has proposition as a type.

Axioms are functions that help us map things to proofs.
Here is an example using modus ponens. Modus ponens is the axiom that, if we prove p implies q, then if p then q. But we can use this axiom as a function type that looks like

Code: Select all

-- Model "a proof of P" and "P implies Q" as opaque constructs.
axiom Proof   : Prop → Type
axiom Implies : Prop → Prop → Prop

-- Modus ponens, stated as an axiom — i.e. a function type.
axiom modus_ponens (p q : Prop) :
  Proof (Implies p q) → Proof p →
  Proof q

Let's break this down one by one. So modus ponens is a function that maps a proof of 'implies p q' to a function proof p -> proof q.

So this means that if we had a proof of (implies p q), and had proof of p, we then do and then this spits out proof q, and so we are done, in a type theoretic way.

Doing this in practice

In practice, we use tactics to actually solve stuff, which I described in an earlier post. The best way I've found to get a strong intuition for tactics is the lean numbers game.

Setting up Lean4 is a bit tricky, so I made a beginner friendly setup script which you can use.

Then, when I want to do some math, the real efficiencies come with using this with Claude. If I am unsure if a proof of mine, I compile the Mathlib and Physlib libraries to get the latest proven math and physics theorem. And the I get Claude code to fill out the proofs in my terminal and have it check that the code compiles. Here's an example of me formally verifying some identities on Hermitian polynomials that I was unsure about with Claude.

So far, I've only used this for math tidbits in my learning process, but it's been useful!

The risk here is that you need to check that the statement you want actually matches the formalisation in Lean. This can be tricky, because many things in math can mean different things, like the word 'differentiable'! But so far it's been a decent aid and I plan to post more on how I've been using it.

References

• Smith, Eric, and Harold J. Morowitz. The Origin and Nature of Life on Earth: The Emergence of the Fourth Geosphere. Cambridge: Cambridge University Press, 2016.
• The mathlib Community. "The Lean Mathematical Library." In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 367–381. New York: ACM, 2020. https://doi.org/10.1145/3372885.3373824
• Tooby-Smith, Joseph. "HepLean: Digitalising high energy physics." Computer Physics Communications 308 (2025): 109457. arXiv:2405.08863. Now developed as PhysLean: https://github.com/HEPLean/PhysLean

[arina]

this feels relevant to the post: https://gwern.net/lean-scaling

[btrettel]

How does Lean compare against computer algebra systems like Maxima and SymPy? Lean seems to intend to be more general and rigorous than computer algebra systems. I have no experience with Lean but quite a bit of experience with Maxima and SymPy. I've checked a lot of derivations for various fluid dynamics models with both, though not without problems.

[casualphysicsenjoyer]

Lean can do proofs beyond just algebraic manipulation - for example proving that a function is continuous, differentiable etc.
My experience is that LEAN is more general, but more of a headache if you want to move symbols around for a derivation.
I am not aware at how good Lean is in doing things that require any approximation scheme though.