The PR to Mathlib #9111 about Spin groups is ready to merge, but there are 2 open questions:

- what more lemmas about Spin groups are interesting to mathematians?
- what more should be formalized to formalize Versors and what’s in Section "The contents of a geometric algebra" in [chisolm2012geometric] , e.g. r-blades, r-vectors?

For the former, I should take a closer look at [figueroa2010spin] and maybe [suarez2019expository], [reynoso2023probing].

For the latter, see the Z-filteration in lean-ga and the prototype.

I also wish to include some latest results presented in [ruhe2023clifford], with supplements from [brehmer2023geometric] (lately there is a new paper applying this in HEP [spinner2024lorentz], in the same spirit, I should also read [berzins2024geometry] and possibly [raissi2019physics]), in which some of the results are proven in [roelfs2023graded].

See also discussions in the lean-ga blueprint.

I've started a Forester experiment about the definitions of Spin groups here. I also need to check citations of On some Lie groups in degenerate Clifford geometric algebras.

The Matrix Cookbook (November 15, 2012) [petersen2008matrix] covers many useful results about matrices, and Eric Wieser's project lean-matrix-cookbook aims to give one-liner proofs (with reference to the counter part in Mathlib) to all of them.

The project is far from complete and it would be great to claim a small portion of interested results and contribute to it. I also wish to figure out the GA counterpart of the same portion.

Previous interests about matrices rise from Steven De Keninck's work on GALM [de2019geometric], since the paper I have been interested in GA approaches that has practical advantages over traditional matrix-based methods. Notably the paper also discussed the link between degenerate Clifford algebras and dual numbers / automatic differentiation. A more recent inspiration might be his new work LookMaNoMatrices.

TODO: decide which results are interesting and feasible to be formalized for me.

I wish to pursue further on the topic of Matrix/Tensor, see [taylor2024introduction] and [randy2023matrix]. The former also led me to Einsums in C++. For the latter, I'm thinking of HepLean.SpaceTime.CliffordAlgebra.

> In a sense, group algebras are the source of all you need to know about representation theory.

The primary reference is [james2001representations] for understanding FG-module, Group algebra, the presentation of groups, Clifford theory (which is the standard method of constructing representations and characters of semi-direct products, see [woit2017quantum], and "3.6 Clifford theory" in [lux2010representations]), Schur indices etc. We also need to check [lux2010representations] for its introduction to GAP, and we should pay close attention to the progress of GAP-LEAN. [sims1994computation] might also be interesting in a similar manner as [lux2010representations] but with emphasis on the presentation of groups.

See also group algebra on nlab, particularly that "A group algebra is in particular a Hopf algebra and a \(G\)-graded algebra."

The related Zulip thread is here, and I have preliminary explorations and experiments in Lean here.

This interest originates from reading Robert A. Wilson's work [wilson2024discrete]. The ultimate goal is to understand the group algebra of the binary tetrahedral group (\(Q_8 \rtimes  Z_3\)), then the three-dimensional complex reflection group (\(G_{27} \rtimes  Q_8 \rtimes  Z_3\)), a.k.a. the triple cover of the Hessian group, which can be interpreted as a finite analogue of the complete gauge group \(U(1) \times  SU(2) \times  SU(3)\).

Recently I have read some meta-level dependent type theory (Typst source). It might be time to re-read `leantt` paper, and start reading `lean4lean` paper/source.

The author `ice1000` has strong interest in QIIT (Quotient Inductive-Inductive Types) and QIIR (Quotient Inductive-Inductive Recursion), he has implemented `overlap` in Aya with termination check and confluence check.

Aya has a philosophy that the kernel could include pattern matching, but at the cost of no generation and translation of eliminators at present. In principle this is feasible, without `overlap`, it could be implemented by "theory of signatures", with `overlap`, it needs "Coherent and concurrent elimination for initial algebras" which I find fascinating, and have read [yeasin2011initial].

The author also has a great article on TT & Cat [zhang2021type]. His recommendation of [gundry2013tutorial] is also worth reading.

In the process of learning Topos, I wish to have a better understanding of Logic. Particularly, Curry–Howard–Lambek correspondance, Propositional truncation, and Paraconsistent logic are on the plate.

Although remotely related, I'll place Introduction to Formal Reasoning (COMP2065) in this section so I won't lose track of it.

Type theories, logic have their origins in philosophy. Lacan had drawn inspiration from the work of the mathematician and philosopher of science Georges Canguilhem, and the philosopher of mathematics Alain Badiou. If he had lived to see the rise of proof assistants, he would be interested in the formalization of his theories.

There is a project on Github called Lacan-Mathemes which visualized some core concepts of Lacan in TikZ. It would be interesting to start there and look for proper objects to formalize in Lean. Another interesting thing to do is to visualize them in Typst.

Here I would like to quote a generated response from Claude 1.2 Instant, which is quite optimistic:

> Here are a few thoughts on formalizing aspects of Lacanian psychoanalytic theory using theorem provers:
>
> - Lacan's structural theory of the psyche could potentially be formalized using logic. The tripartite structure of the Real, Symbolic, and Imaginary could be modeled as formal domains or ontologies with defined relationships between them.
> - Key concepts like the mirror stage, the Name-of-the-Father, the objet petit a, etc. could be defined as logical predicates or functions operating within this structural framework. For example, one could define predicates like "inMirrorStage(subject)" or "desiresObjetPetitA(subject, object)".
> - Relations like the split between desire and drive, the tension between the Symbolic order and the Real, the misrecognition of the Imaginary could be expressed through logical rules and inferences between concepts.
> - The dynamics of psychoanalytic concepts like repression, sublimation, transference could be modeled as state transitions or logical transformations within the structured system.
> - Specific psychoanalytic theories like the stages of psychosexual development or the topology of the fantasy could be axiomatized and theorems deduced from the axioms.
>
> However, capturing the open-ended, non-deterministic nature of unconscious processes and the ambiguity/contingency of signification would be challenging and may require non-classical logics or probabilistic approaches.
>
> So in summary, while difficult, certain aspects of Lacanian theory seem amenable to formalization using tools from logic, ontology, and knowledge representation. Careful design would be needed to address theory's complexity.

Lately there is a paper formalizing Kant [achourioti2011formalization] which might be interesting.

A categorical view of Clifford Algebra is discussed in [figueroa2010spin].

A Clifford Algebra can be categorified: "An Clifford algebra over a vector space is defined to be the Koszul dual to an abelian fully weak Lie-algebra" where "Fully weak Lie-algebras are Koszul dual to differential graded Clifford algebras." See also Higher Clifford Algebras.

Sheaves of Clifford Algebras are studied in [yizengaw2015clifford] and its references. See also [schapira2023introduction], an elementary introduction to [kashiwara2006categories], which presents categories, homological algebra and sheaves in a systematic and exhaustive manner.

Duffin-Kemmer-Petiau Algebra is

\[\frac {T(V)}{I(v\otimes  w\otimes  v - g(v,w)v)}\]

in the same way that Clifford Algebra is

\[\frac {T(V)}{I(v\otimes  v - g(v,v))}.\]

See [fernandes2022clifford] which embeds DKP Algebra in Clifford Algebra with projectors.

TODO:

- Recovering Composition Algebras from 3D Geometric Algebras
- Eliminating topological errors in neural network rotation estimation using self-selecting ensembles - Sitao Xiang - SIGGRAPH 2021
- OSMU24: Quantum Foundations, Particle Physics, and Unification of Forces
- Bill Baylis' research on Clifford's Geometric Algebra of Physical Space (APS)

See [manturov2018knot] and the tracking issue.

For interpreting knots in a sheaf-theoretic perspective, see [chrisman2023geometric].

See also:

- A Table of Virtual Knots
- The homological arrow polynomial for virtual links (code)

My first impression of sheaves is that they are useful to local-to-global applications "which ask for global solutions to problems whose hypotheses are local".

Roughly speaking, a sheaf requires some gluing conditions (axioms "Locality" and "Gluing") so that local data can be collated compatibly into a global algebraic structure that varies continuously over local covering domains ("sections" of sheaves).

To do so, a sheaf in general, as defined in the category-theoretical language, needs

- a topological space (or a site in general), denoted \(X\) (or \(\mathcal {C}\) for a site)
- a category, sometimes denoted \(\mathcal {D}\), meaning "data category", whose objects are algebraic structures and morphisms are structure-preserving maps

and builds (gluing conditions) on a \(\mathcal {D}\)-valued presheaf over \(X\) (or \(\mathcal {C}\)), denoted \(\mathcal {F}\) (as its French name is "faisceau"), which is essentially a  contravariant functor \(\mathcal {F}: \mathcal {C}^{op} \to  \mathcal {D}\) but a concept with an attitude, and its morphisms are restriction maps between open sets in \(X\) (or between objects that satisfy the pretopology \(\mathcal {J}\) in \(C\), where \(\mathcal {J}\) is the pretopology on \(\operatorname {Open}(X)\), which specifies when a covering family of open sets exists).

Its latest application to deep learning, Thomas Gebhart's thesis [gebhart2023sheaf] sees a sheaf over a topological space as a data structure "which defines rules for associating data to a space so that local agreements in data assignment align with a coherent global representation", thus a generalization of both:

- relational learning, which aims to "combine symbolic, potentially hand-engineered prior knowledge with the tabula rasa representational flexibility of deep learning to achieve a synthetic model family which can be defined with respect to symbolic knowledge priors about the data domain"
- geometric deep learning, which "provides a group-theoretic approach to reasoning about and encoding domain-symmetry invariance or equivariance within machine learning models",

"providing a mathematical framework for characterizing the interplay between the topological information embedded within a domain and the representations of data learned by machine learning models".

My prior interest in geometric deep learning, particularly group-equivariant neural networks, and my believe in symbolism, are the background of my interest in sheaf representation learning.

Notably, this thesis treats the discrete case of sheaves, a cellular sheaf, whose

- topological space is a cell complex, which is "a topological generalization of a graph, with set inclusion and intersection given by the incidence relationships among cells in the complex", thus "admitting a computable, linear-algebraic representation".
- data category is \(\mathtt {FVect}\), the category of finite-dimensional vector spaces over a field \(\mathbb {F}\), which is a common choice for the data category in machine learning applications, a model-free approach with massive parameter space, flexible representational capacity, but inherits fundamental limitations, e.g. data inefficiency, generalization failure, and interpretability issues.

For more details, see also Thomas Gebhart's talk Sheaves for AI: Graph Representation Learning through Sheaf Theory.

<!-- has the potential to learn sheaf representations of data, which is essentially assigning observed data to a space in a way that's

globally consistent with the constraints imposed by the topology of the application domain .

a richer but still tractable representation that is an algebraic structure richer than a vector space commonly used in ML, to sampled data, which is in the form of components of a category (e.g. a category of a data structure like a Graph).  -->

Its application to physics has the potential to formulate differential geometry in a more general setting, without assuming the existence of a locally Euclidean space as manifold did. It's believe that this approach can overcome some difficulties in Quantum field theory even Quantum gravity, because locally there might be no concept of a metric space at all [mallios2015differential].

Note that there are CAS systems that can do sheaf cohomology etc., e.g. Macaulay2, OSCAR.

For SDG, [kock2006synthetic] is a classic. [schellingerhout2023circles] is a concise bachelor thesis on the topic, and has interesting discussions on circles.

Ryszard Paweł Kostecki has very approachable notes on Topos [kostecki2011introduction] and SDG [kostecki2009differential].

We should also read [rosiak2022sheaf]. It also has many diagrams in the way I imagined, for examples of sheaf.

I don't want efforts in Transformers: from self-attention to performance optimizations to be discontinued, lately there is [ferrando2024primer] on this topic.

I might need to follow on the latest development on the linear attention mechanism [peng2024eagle].

I have almost no understanding of diffusion models, so I should read [bao2023all] and related papers.

I should also read [mikula2023magnushammer] and related papers.