Project Ideas

Similar to the current formalization of the classical harmonic oscillator, this project corresponds to the formalization of a pendulum.

Formalize Planck's law for blackbody radiation, and derive Wien's displacement law.

Formalize the solution to a system of binary stars.

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.

Formalize the properties of the reflectionless potential in quantum mechanics, following the formalization of the quantum harmonic oscillator.

Physlib already contains the tight-binding model for a chain. This project would aim to generalize that to do the tight-binding model for graphene.

Define the Hilbert space of a single bosonic and a single fermionic particle. Part of this will involve defining the Lorentz-invariant measure and the mass-shell manifold.

Within Physlib there are currently some informal results related to the FLRW metric. The aim of this project would be to formalize those results into Lean and expand upon them.

Write down and prove the basic properties of Laplace's tidal equations. One could go further and provide a derivation of these equations.

Write down the Boltzmann equation with the BGK collision operator and prove basic properties about solutions thereof.

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.

Formalize the quantum mechanics of a particle on a ring.

Prove Theorem 1, 2 & 4 of 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.

Prove the group theoretic properties of the grand-unified theories: SU(5), Spin(10) and Pati-Salam.