leanprover-community / leanprover-community/physlib
Formalization: Beyond the standard model gauge groups
Open
Nobody has claimed this yet.
formalization
help-wanted
- Dominant language
- Lean
- Stars
- 749
- Forks
- 189
- Avg merge
- 1d 21h
- Merged PRs (30d)
- 75
Description
In the formalization of beyond the standard model gauge groups, there are the following TODO items:
Georgi-Glashow Model
- informal_def (6V2WM): GeorgiGlashow.GaugeGroupI
- informal_def (6V2WS): GeorgiGlashow.inclSM
- informal_lemma (6V2W2): GeorgiGlashow.inclSM_ker
- informal_def (6V2XA): GeorgiGlashow.embedSMℤ₆
Pati-Salam
- informal_def (6V2Q2): PatiSalam.GaugeGroupI
- informal_def (6V2RH): PatiSalam.inclSM
- informal_lemma (6V2RQ): PatiSalam.inclSM_ker
- informal_def (6V2RY): PatiSalam.embedSMℤ₃
- informal_def (6V2R7): PatiSalam.gaugeGroupISpinEquiv
- informal_def (6V2SG): PatiSalam.gaugeGroupℤ₂SubGroup
- informal_def (6V2SM): PatiSalam.GaugeGroupℤ₂
- informal_lemma (6V2SV): PatiSalam.sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup
- informal_def (6V2S4): PatiSalam.embedSMℤ₆Toℤ₂
Spin(10) model (aka SO(10) model)
- informal_def (6V2S4): PatiSalam.embedSMℤ₆Toℤ₂
- informal_def (6V2YG): Spin10Model.inclPatiSalam
- informal_def (6V2YO): Spin10Model.inclSM
- informal_def (6V2YU): Spin10Model.inclGeorgiGlashow
- informal_def (6V2YZ): Spin10Model.inclSMThruGeorgiGlashow
- informal_lemma (6V2Y6): Spin10Model.inclSM_eq_inclSMThruGeorgiGlashow
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the linked TODOList entries for the Georgi-Glashow, Pati-Salam, and Spin(10) models, especially the named definitions and lemmas. Determine the required formal statements from those entries; done means the listed TODO items are formally defined or proved and no longer remain outstanding.
Written by the indexing model from the issue text.
Assessment
- Domain
- devtools
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 25/100