navigation / documentation overview / Hilbert's Sixth Problem
How is the Physics Derivation Graph related to Hilbert's Sixth Problem?
Hilbert's Sixth Problem is
"To treat in the same manner, by means of axioms, those physical sciences in which already today mathematics plays an important part; in the first rank are the theory of probabilities and mechanics."
Solving, or even attempting to solve, that challenge is ambitious. Whether the inference rules would qualify as axioms is not clear to the developer of the Physics Derivation Graph. Writing down all of mathematical physics is the primary goal of the Physics Derivation Graph, and the fact that some of the steps can be proven in Lean is an accidental benefit. The use of a Computer Algebra System (CAS) like SymPy and a proof assistant like Lean are secondary in the Physics Derivation Graph because the author does not expect every inference rule to be amenable to rigorous validation.
Hilbert explicitly included probability theory in his request, as it was essential for the kinetic theory of gases. In 1933, the Russian mathematician Andrey Kolmogorov published Foundations of the Theory of Probability. He successfully axiomatized probability using measure theory.
Hilbert wanted a rigorous mathematical explanation of how the behavior of atoms (microscopic) leads to the laws of fluid dynamics (macroscopic). Specifically, he wanted to derive the Euler and Navier-Stokes equations directly from the Boltzmann equation. The challenge is proving that the chaotic motion of billions of particles mathematically converges to smooth fluid flows without logical gaps. Provide a complete, rigorous proof that the continuum mechanics of fluids emerges from atomistic dynamics under all conditions (including turbulence).
axiomatize Quantum Field Theory (QFT). Solve the Yang-Mills Existence and Mass Gap problem. This is one of the Clay Millennium Prize problems. Prove that the mathematical governing equations of particle physics exist and have a "mass gap" (meaning particles have mass) using strict axiomatic standards.
Hilbert wanted the axioms of all physics. Currently, physics is broken into two incompatible frameworks:
Need a theory of Quantum Gravity. Candidates include String Theory and Loop Quantum Gravity, but neither has been experimentally verified or fully axiomatized. Once a unified physical theory is discovered, then formulate it as a set of axioms from which all physical phenomena can be derived as theorems.