diff --git a/docs/_data/TODO.yml b/docs/_data/TODO.yml
new file mode 100644
index 00000000..43f42f55
--- /dev/null
+++ b/docs/_data/TODO.yml
@@ -0,0 +1,190 @@
+##
+# This file is generated by the `lake exe TODO_to_yml mkFile` command.
+# Do not edit manually.
+- content: "Refactor whole file, and dependent files."
+  file: HepLean.AnomalyCancellation.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/Basic.lean#L19
+  line: 19
+
+- content: "Relate ACC Systems to algebraic varieties."
+  file: HepLean.AnomalyCancellation.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/Basic.lean#L18
+  line: 18
+
+- content: "Derive an ACC system from a guage algebra and fermionic representations."
+  file: HepLean.AnomalyCancellation.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/Basic.lean#L17
+  line: 17
+
+- content: "replace `Finsupp.equivFunOnFinite` here with `Finsupp.linearEquivFunOnFinite`."
+  file: HepLean.AnomalyCancellation.PureU1.BasisLinear
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean#L78
+  line: 78
+
+- content: "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`."
+  file: HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean#L619
+  line: 619
+
+- content: "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`."
+  file: HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean#L626
+  line: 626
+
+- content: "Replace the definition of `pairSwap` with `Equiv.swap`."
+  file: HepLean.AnomalyCancellation.PureU1.Permutations
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/Permutations.lean#L92
+  line: 92
+
+- content: "Define vector like ACC in the `n`-odd case."
+  file: HepLean.AnomalyCancellation.PureU1.VectorLike
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/VectorLike.lean#L13
+  line: 13
+
+- content: "Prove bounded properties of the 2HDM potential.
+  See e.g. https://inspirehep.net/literature/201299 and
+  https://arxiv.org/pdf/hep-ph/0605184."
+  file: HepLean.BeyondTheStandardModel.TwoHDM.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean#L148
+  line: 148
+
+- content: "Define the standard basis of the Lorentz algebra."
+  file: HepLean.Lorentz.Algebra.Basis
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Algebra/Basis.lean#L19
+  line: 19
+
+- content: "Generalize `basis_eq_FD`."
+  file: HepLean.Lorentz.ComplexTensor.Basis
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/ComplexTensor/Basis.lean#L51
+  line: 51
+
+- content: "Work out why `pauliCo_prod_basis_expand'` is needed."
+  file: HepLean.Lorentz.ComplexTensor.PauliMatrices.CoContractContr
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean#L391
+  line: 391
+
+- content: "Include relation to real Lorentz vectors."
+  file: HepLean.Lorentz.ComplexVector.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/ComplexVector/Basic.lean#L144
+  line: 144
+
+- content: "Rename."
+  file: HepLean.Lorentz.ComplexVector.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/ComplexVector/Basic.lean#L132
+  line: 132
+
+- content: "Show that the Lorentz group is a Lie group."
+  file: HepLean.Lorentz.Group.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Basic.lean#L18
+  line: 18
+
+- content: "Show that generalised boosts are in the restricted Lorentz group."
+  file: HepLean.Lorentz.Group.Boosts
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Boosts.lean#L24
+  line: 24
+
+- content: "Prove topological properties of the Orthochronous Lorentz Group."
+  file: HepLean.Lorentz.Group.Orthochronous
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Orthochronous.lean#L15
+  line: 15
+
+- content: "Prove restricted Lorentz group equivalent to connected component of identity."
+  file: HepLean.Lorentz.Group.Restricted
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Restricted.lean#L15
+  line: 15
+
+- content: "Add definition of the restricted Lorentz group."
+  file: HepLean.Lorentz.Group.Restricted
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Restricted.lean#L13
+  line: 13
+
+- content: "Prove member of the restricted Lorentz group is combo of boost and rotation."
+  file: HepLean.Lorentz.Group.Restricted
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Restricted.lean#L14
+  line: 14
+
+- content: "Generalize the inclusion of rotations into LorentzGroup to abitary dimension."
+  file: HepLean.Lorentz.Group.Rotations
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Rotations.lean#L14
+  line: 14
+
+- content: "Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group."
+  file: HepLean.Lorentz.SL2C.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/SL2C/Basic.lean#L315
+  line: 315
+
+- content: "Replace the definitions in this file with Mathlib definitions."
+  file: HepLean.Mathematics.LinearMaps
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Mathematics/LinearMaps.lean#L17
+  line: 17
+
+- content: "Make this definition more functional in style."
+  file: HepLean.Meta.AllFilePaths
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Meta/AllFilePaths.lean#L16
+  line: 16
+
+- content: "Can likely make this a bona-fide command."
+  file: HepLean.Meta.Informal.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Meta/Informal/Basic.lean#L20
+  line: 20
+
+- content: "Find a way to free the environment `env` in `transverseTactics`.
+  This leads to memory problems when using `transverseTactics` directly in loops."
+  file: HepLean.Meta.TransverseTactics
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Meta/TransverseTactics.lean#L78
+  line: 78
+
+- content: "Split the following two lemmas up into smaller parts."
+  file: HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean#L374
+  line: 374
+
+- content: "SpaceTime should be refactored into a structure, to prevent casting."
+  file: HepLean.SpaceTime.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/SpaceTime/Basic.lean#L18
+  line: 18
+
+- content: "Prove algebra generated by gamma matrices is isomorphic to Clifford algebra."
+  file: HepLean.SpaceTime.CliffordAlgebra
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/SpaceTime/CliffordAlgebra.lean#L14
+  line: 14
+
+- content: "Define relations between the gamma matrices."
+  file: HepLean.SpaceTime.CliffordAlgebra
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/SpaceTime/CliffordAlgebra.lean#L15
+  line: 15
+
+- content: "Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆."
+  file: HepLean.StandardModel.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/Basic.lean#L15
+  line: 15
+
+- content: "Make `HiggsBundle` an associated bundle."
+  file: HepLean.StandardModel.HiggsBoson.Basic
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/Basic.lean#L82
+  line: 82
+
+- content: "Define the global gauge action on HiggsField."
+  file: HepLean.StandardModel.HiggsBoson.GaugeAction
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/GaugeAction.lean#L239
+  line: 239
+
+- content: "Prove invariance of potential under global gauge action."
+  file: HepLean.StandardModel.HiggsBoson.GaugeAction
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/GaugeAction.lean#L241
+  line: 241
+
+- content: "Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary)"
+  file: HepLean.StandardModel.HiggsBoson.GaugeAction
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/GaugeAction.lean#L240
+  line: 240
+
+- content: "Currently this only contains the action of the global gauge group. Generalize."
+  file: HepLean.StandardModel.HiggsBoson.GaugeAction
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/GaugeAction.lean#L16
+  line: 16
+
+- content: "Find a better place for this."
+  file: HepLean.Tensors.OverColor.Discrete
+  githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Tensors/OverColor/Discrete.lean#L159
+  line: 159