Mini projects

Stream: PhysLean

[Joseph Tooby-Smith]

For people interested in contributing to HepLean, but don't know where to start or what to do, I am going to use this thread to post mini project ideas. This is in addition to what HepLean currently has in the form of:

• A TODO list
• A graph of informal lemmas

which can also be used as a source of ideas of how to contribute.

Also if you have ideas for mini projects suitable for HepLean but you do not have the time or capacity to do them yourself please post them here.

[Joseph Tooby-Smith]

The two-higgs doublet model potential

Aim: Prove Theorem 1, 2 & 4 of this paper: https://arxiv.org/pdf/hep-ph/0605184, or variations of.

Physics context: The two-Higgs doublet model is a model of the universe with a proposed extra Higgs boson - giving two Higgs fields in total. Associated with these two Higgs fields is a potential whose minimum and boundness is very important to physics (it is what determines mass in the universe). The theorems in the above paper prove results related to these minima and boundness properties.

Math context: The actual maths involved is simple algebraic manipulation with potentially a small bit of calculus and group theory.

Current progress: Some of the set-up is already in HepLean but not much substantial progress has been made to proving these results.

Note: I don't believe you need to know much/any physics to do this project.

[Joseph Tooby-Smith]

Properties of grand unified theory groups

Aim: Prove group theoretic properties of the grand unified theories: SU(5), Spin(10) and Pati-Salam. Examples of such properties can be found in https://math.ucr.edu/home/baez/guts.pdf. They also appear as informal results in HepLean. See e.g. here.

Physics context: Grand unified theories are popular models beyond the standard model which unify all the fermions into the universe into the representation of a semi-simple or simple Lie group.

Math context: Group theory of several low-dimensional Lie groups (don't actually need Lie group structures) and maps between them.

Note: Like the project above, I don't believe you need to know much/any physics for this.

[Joseph Tooby-Smith]

Properties of Pauli matrices

Aim: Prove the properties of the Pauli matrices in Eq. 2.23 - 2.30 of this using index notation. An example of a similar calculation already in HepLean is this calculation.

[Joseph Tooby-Smith]

A start on optics

Aim: To convert the relevant parts of this into Lean.