validate derivation step using Lean

[bhpayne]

Lean is now in the webserver Docker image so steps can be validated.

The repo https://github.com/allofphysicsgraph/lean-in-docker/tree/main/lean_v4 is for exploring how to validate a step.

A simple example would be applying the inference rule "add X to both sides" of a+b to get a+2 = b+2.

In Lean, a=b is a proposition. We have to specify that a is Real and b is Real. Then we can prove that
(a=b) -> (a+2=b+2).

The relation between PDG and Lean is described here: https://physicsderivationgraph.blogspot.com/2023/06/translating-between-physics-derivation.html

[bhpayne]

Review https://stackoverflow.com/questions/41946310/how-to-prove-a-b-%E2%86%92-a-1-b-1-in-lean