Initially the Physics Derivation Graph documented expressions as Latex. Then SymPy was added to support validation of steps (is the step self-consistent) and dimensionality (is the expression self-consistent?).
Recently I learned that Lean could be used to prove each step in a derivation. The difference between a Computer Algebra System (e.g., SymPy) and Lean is whether "a = b --> a/b = 1" is a valid step -- it isn't when b is zero. Lean catches that; SymPy does not.
While Lean proofs sound like the last possible refinement, there are two additional complications to account for not addressed by Lean.
Challenge: Bounded ranges of applicability
In classical mechanics the relation between momentum, mass, and velocity is "p = m v". That hold when "v << c". Near the speed of light we need to switch to relativistic mass,
m = m_{rest} / sqrt{1-((v^2)/(c^2))}.
The boundary between "v << c" and "v ~ c" is usually set by the context being considered.
One response for users of Lean would be to always use the "correct" relativistic equation, even when "v << c." A more conventional approach used by Physicists is to use
p = m v, where v << c
then drop the "v << c" clause and rely on context.
Challenge: Real versus Float versus experimental characterization
Lean forces you to characterize numbers as Real or Integer or Complex. This presents a problem for numerical simulations that have something like a 64 bit float representation.
In thermodynamics we assume the number of particles involved is sufficiently large that we focus on the behavior of the ensemble rather than individual particles. The imprecision of floats is not correct, but neither is the infinite precision assumed by Real numbers.
Example applications of Lean proofs needing bounds on values
Math doesn't have convenient ways of indicating "finite precision, as set by the Plank scale." The differential element used in calculus cannot actually go to zero, but we use that concept because it works at the scales we are used to.
Physicists make simplifying assumptions that sometimes ignore reality (e.g., assuming continuous media when particles are discrete). Then again the assumption that particles are discrete is also a convenient fiction that ignores the wavefunction of quantum mechanics.
Lean can be used to prove derivations in classical mechanics, but to be explicit about the bounds of those proofs we'd also need to indicate "v << c" and "assume space is Euclidean."
For molecular dynamics, another constraint to account for is "temperature << 1E10 Kelvin" or whatever temperature the atoms breaks down into plasma.
Distinguishing the context of (classical mechanics from quantum) and (classical from relativistic) and (conventional gas versus plasma) seems important so that we know when a claim proven in Lean is applicable.
