Project ideas
Below are a list of project ideas, no matter who you are, you may attempt any of these. You should assume that this list is up-to date. They are roughly ordered in complexity from easiest to hardest. If you would like to ‘claim’ one of these projects or add projects let Joseph Tooby-Smith know, or make a pull-request to the PhysLean website repo.
Classical mechanics of a pendulum
Available
Similar to the current formalization of the classical harmonic oscillator, this project corresponds to the formalization of pendulum. The Wikipedia page here has more details.
Planck’s theory of blackbody radiation
Available
Formalize Planck’s law (see here) for blackbody radiation, and derive Wien’s displacement law (see here).
Binary star system
Available
Formalize the solution to a system of binary stars, see e.g. this.
Hydrodynamic drag
Available
Write down Newton’s second law for a particle with a hydrodynamic drag trapped in a harmonic spring, and derive from that a differential equation for the mean-squared displacement. See here.
The reflectionless potential in quantum mechanics
Available
Formalize the properties of the reflectionless potential in quantum mechanics, following the formalization of the quantum harmonic oscillator.
Tight-binding model for graphene
Available
PhysLean already contains the tight-binding model for a chain. This project would aim to generalize that to do the tight-binding model for graphene. A reference can be found here.
Definition of the bosonic and fermionic Hilbert spaces
Available
Define the Hilbert space of a single bosonic and a single fermionic particle. These can be found in these note. Part of this will involve defining the Lorentz-invariant measure and the mass-shell manifold.
Basic properties of cosmology
Available
Within PhysLean there are currently some informal results related to the FLRW metric, these appear in this file. The aim of this project would be to formalize into Lean those results, and expand upon them. See a related discussion here.
Laplace’s tidal equations
Available
Write down and prove the basic properties of Laplace’s tidal equations, see e.g. here. One could go further, and provide a derivation of these equations.
Boltzmann equation
Available
Write down the Boltzmann equation with the BGK collision operator and prove basic properties about solutions thereof. See, amongst other places, this.
Larmor formula (Power radiated by a non-relativistic particle)
Available
The Larmor formula gives the power radiated by a non-relativistic point particle as it accelerates. The idea of this project would be to derive this formula using the foundations of electromagnetism.
Quantum particle on a ring
Available
Formalize the quantum mechanics of a particle on a ring, see e.g. the wikipedia page. See also, this Zulip discussion.
The two Higgs doublet model potential
Available
The aim of this project would be to prove Theorem 1, 2 & 4 of this arXiv(hep-ph):0605184. This is related to the two Higgs doublet model, which corresponds to a model of the universe with a proposed extra Higgs doublet.
Properties of grand unified theory groups
Available
Prove the group theoretic properties of the grand-unified theories: SU(5), Spin(10) and Pati-Salam, as they appear in this note. Some of these results appear on the todo list.