Port: My math interests in 2024

assets/uts-overrides.xsl

@@ -7,7 +7,7 @@
                 xmlns:f="http://www.jonmsterling.com/jms-005P.xml"
                 xmlns:html="http://www.w3.org/1999/xhtml"
     >
-    
+
     <!-- <xsl:template name="numbered-taxon">
         <span class="taxon">
             <xsl:apply-templates select="f:taxon" />
@@ -238,4 +238,16 @@
         <xsl:text>]]))</xsl:text>
     </xsl:template>
 
-</xsl:stylesheet>
+    <!-- A simple hack to make f:tex pass through markdown-it, but not handling more escape cases yet -->
+    <!-- <xsl:template match="html:div[@class='markdownit grace-loading']//f:tex[@display='block']">
+    <xsl:text>\\[</xsl:text>
+    <xsl:value-of select="." />
+    <xsl:text>\\]</xsl:text>
+    </xsl:template>
+    <xsl:template match="html:div[@class='markdownit grace-loading']//f:tex[not(@display='block')]">
+    <xsl:text>\\(</xsl:text>
+    <xsl:value-of select="." />
+    <xsl:text>\\)</xsl:text>
+    </xsl:template> -->
+
+</xsl:stylesheet>

bun/markdownit.js

@@ -10,6 +10,14 @@ for (let i = 0; i < markdownit_tags.length; i++) {
     const markdownit_tag = markdownit_tags[i]
     const markdown_source = markdownit_tag.innerHTML
     // console.log(markdown_source);
-    markdownit_tag.innerHTML = md.render(markdown_source)
+    const converted_source = markdown_source
+        .replaceAll(/&lt;/g, '<')
+        // unescape to make quotes work
+        .replaceAll(/&gt;/g, '>')
+        // we escape fr:tex tags to avoid conflicts with markdown syntax
+        // note that we need to use `+?` which is a lazy quantifier, meaning it matches as few characters as possible
+        .replaceAll(/\\([\[\(])(.+?)\\([\)\]])/g, '\\\\$1$2\\\\$3')
+    console.log(converted_source)
+    markdownit_tag.innerHTML = md.render(converted_source)
     markdownit_tag.classList.remove('grace-loading')
 }

tex/forest.bib

@@ -1097,3 +1097,10 @@ @article{paszke2021getting
   year={2021},
   publisher={ACM New York, NY, USA}
 }
+
+@article{wu2024multi,
+  title={A Multi-Level Superoptimizer for Tensor Programs},
+  author={Wu, Mengdi and Cheng, Xinhao and Padon, Oded and Jia, Zhihao},
+  journal={arXiv preprint arXiv:2405.05751},
+  year={2024}
+}

trees/macros.tree

@@ -527,13 +527,11 @@ so the text size almost matches the size output by native forester code. This do
   }
 }
 
-\def\md[body]{
-  \<html:div>[class]{markdownit grace-loading}{\body}
-}
+\def\md[body]{\<html:div>[class]{markdownit grace-loading}{\body}}
 
-\def\mdblock[t][body]{
-  \block{\t}{\<html:div>[class]{markdownit grace-loading}{\body}}
-}
+\def\mdblock[t][body]{\block{\t}{\md{\body}}}
+
+\def\mdnote[t][body]{\note{\t}{\md{\body}}}
 
 \def\loadjs[src]{
   \<html:script>[type]{module}[src]{\src}{}

trees/refs/fernandes2022clifford.tree

@@ -1,13 +1,13 @@
-% ["math-2024"]
-\title{Clifford algebraic approach to the de donder–weyl hamiltonian theory}
+% ["manual", "math-2024"]
+\title{Clifford Algebraic Approach to the De Donder-Weyl Hamiltonian Theory}
 \date{2022}
 \author{Marco Cezar Barbosa Fernandes}
 \taxon{reference}
 \meta{external}{https://arxiv.org/pdf/2112.08483}
 
 \meta{bibtex}{\startverb
 @article{fernandes2022clifford,
- title = {Clifford Algebraic Approach to the De Donder--Weyl Hamiltonian Theory},
+ title = {Clifford Algebraic Approach to the De Donder-Weyl Hamiltonian Theory},
  author = {Fernandes, Marco Cezar Barbosa},
  year = {2022},
  url = {https://arxiv.org/pdf/2112.08483},

trees/refs/wu2024multi.tree

@@ -0,0 +1,14 @@
+% ["forest"]
+\title{A multi-level superoptimizer for tensor programs}
+\date{2024}
+\author{Mengdi Wu}\author{Xinhao Cheng}\author{Oded Padon}\author{Zhihao Jia}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@article{wu2024multi,
+ title = {A Multi-Level Superoptimizer for Tensor Programs},
+ author = {Wu, Mengdi and Cheng, Xinhao and Padon, Oded and Jia, Zhihao},
+ year = {2024},
+ journal = {arXiv preprint arXiv:2405.05751}
+}
+\stopverb}

trees/uts-0018.tree

@@ -17,6 +17,7 @@
 \mdblock{10-07}{
 - learned about [lobste.rs](https://lobste.rs/), a computing-focused community centered around link aggregation and discussion, a bit like Hacker News but less noise maybe
 - read [Rewriting Rust](https://lobste.rs/s/29a1eo/rewriting_rust) and [Josh Triplett's comment](https://www.reddit.com/r/rust/comments/1fpomvp/rewriting_rust/lozktuv/)
+- read \citek{wu2024multi} and learn about [mirage](https://github.com/mirage-project/mirage)
 }
 
 \mdblock{10-06}{

trees/uts-001R.tree

@@ -0,0 +1,23 @@
+\import{macros}
+% clifford hopf spin tt ag math draft tech exp notes
+\tag{math}
+\tag{notes}
+
+\author{utensil}
+\date{2024-03-16}
+
+\note{My math interests in 2024}{
+
+\quote{Initially posted [here](https://utensil.github.io/blog/posts/math-2024/), moved here for updates.}
+
+\transclude{uts-001S}
+\transclude{uts-001T}
+\transclude{uts-001Z}
+\transclude{uts-0024}
+\transclude{uts-002D}
+\transclude{uts-002E}
+}
+
+% porting note:
+% replace \{\{<cite "([^"]+)">\}\} to \citek{$1} modulo spaces
+% replace \$([^$]+)\$ to #{$1} with manual fixes for ##{} cases

trees/uts-001S.tree

@@ -0,0 +1,11 @@
+\import{macros}
+
+\mdnote{Rationale}{
+I wish this post to be a continuously updated list of my math interests in 2024 with proper citations to literatures, as I keep wandering in the math wonderland and I don't want to be lost in it without breadcrumbs.
+
+Some interests that have older origins will gradually moved to corresponding posts for earlier years.
+
+I also hope certain interests will be developed into research projects, and leaving only a brief summary and a link here.
+
+Each interest should have one or few central questions, and one or few references to literatures.
+}

trees/uts-001T.tree

@@ -0,0 +1,12 @@
+\import{macros}
+
+\note{Formalization}{
+\md{
+This part of interests is about small-scale formalization of mathematical concepts and theorems, for learning and potential PRs to Lean's Mathlib. Each should focus on one reference which is well organized and convenient to be converted into a blueprint.
+}
+
+\transclude{uts-001U}
+\transclude{uts-001V}
+\transclude{uts-001W}
+\transclude{uts-001X}
+}

trees/uts-001U.tree

@@ -0,0 +1,18 @@
+\import{macros}
+
+\mdnote{Spin groups}{
+The PR to Mathlib [#9111](https://github.com/leanprover-community/mathlib4/pull/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 \citek{chisolm2012geometric} , e.g. r-blades, r-vectors?
+
+For the former, I should take a closer look at \citek{figueroa2010spin} and maybe \citek{suarez2019expository}, \citek{reynoso2023probing}.
+
+For the latter, see the [Z-filteration in lean-ga](https://github.com/pygae/lean-ga/blob/master/src/geometric_algebra/from_mathlib/versors.lean) and [the prototype](https://github.com/eric-wieser/lftcm2023-clifford_algebra/).
+
+I also wish to include some latest results presented in \citek{ruhe2023clifford}, with supplements from \citek{brehmer2023geometric} (lately there is a new paper applying this in HEP \citek{spinner2024lorentz}, in the same spirit, I should also read \citek{berzins2024geometry} and possibly \citek{raissi2019physics}), in which some of the results are proven in \citek{roelfs2023graded}.
+
+See also discussions in the [lean-ga blueprint](https://utensil.github.io/lean-ga/blueprint/sect0007.html).
+
+I've started a Forester experiment about the definitions of Spin groups [here](https://utensil.github.io/forest/spin-0001.xml). I also need to check citations of [On some Lie groups in degenerate Clifford geometric algebras](https://arxiv.org/abs/2301.06842).
+}

trees/uts-001V.tree

@@ -0,0 +1,13 @@
+\import{macros}
+
+\mdnote{Matrix}{
+The Matrix Cookbook (November 15, 2012) \citek{petersen2008matrix} covers many useful results about matrices, and Eric Wieser's project [lean-matrix-cookbook](https://github.com/eric-wieser/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 \citek{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](https://github.com/enkimute/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 \citek{taylor2024introduction} and \citek{randy2023matrix}. The former also led me to [Einsums in C++](https://github.com/Einsums/Einsums). For the latter, I'm thinking of [HepLean.SpaceTime.CliffordAlgebra](https://github.com/HEPLean/HepLean/blob/master/HepLean/SpaceTime/CliffordAlgebra.lean).
+}

trees/uts-001W.tree

@@ -0,0 +1,13 @@
+\import{macros}
+
+\mdnote{Group Algebra}{%
+> In a sense, group algebras are the source of all you need to know about representation theory.
+
+The primary reference is \citek{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 \citek{woit2017quantum}, and "3.6 Clifford theory" in \citek{lux2010representations}), Schur indices etc. We also need to check \citek{lux2010representations} for its introduction to [GAP](https://www.gap-system.org/), and we should pay close attention to the progress of [GAP-LEAN](https://github.com/opencompl/lean-gap). \citek{sims1994computation} might also be interesting in a similar manner as \citek{lux2010representations} but with emphasis on the presentation of groups.
+
+See also [group algebra on nlab](https://ncatlab.org/nlab/show/group+algebra), particularly that "A group algebra is in particular a Hopf algebra and a #{G}-graded algebra."
+
+The related Zulip thread is [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Group.20algebra.20over.20finite.20groups), and I have preliminary explorations and experiments in Lean [here](https://github.com/utensil/lean-playground/blob/master/lean4/examples/FiniteGroup.lean).
+
+This interest originates from reading Robert A. Wilson's work \citek{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)}.
+}

trees/uts-001X.tree

@@ -0,0 +1,15 @@
+\import{macros}
+
+\mdnote{Type Theory}{
+Recently I have read [some meta-level dependent type theory](https://ice1000.org/) ([Typst source](https://github.com/ice1000/website/tree/main/dtt-dev)). 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](https://github.com/aya-prover/aya-dev/pull/1042) with [termination check and confluence check](https://github.com/aya-prover/aya-dev/blob/main/cli-impl/src/test/resources/negative/PatCohError.txt).
+
+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 \citek{yeasin2011initial}.
+
+The author also has a great article on TT & Cat \citek{zhang2021type}. His recommendation of \citek{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](\verb!|https://www.bananaspace.org/wiki/%E7%B1%BB%E5%9E%8B%E8%AE%BA%E2%80%93%E8%8C%83%E7%95%B4%E8%AE%BA%E2%80%93%E9%80%BB%E8%BE%91%E5%AD%A6%E7%B1%BB%E6%AF%94!), [Propositional truncation](https://1lab.dev/1Lab.HIT.Truncation.html#propositional-truncation), and [Paraconsistent logic](https://en.wikipedia.org/wiki/Paraconsistent_logic) are on the plate.
+
+Although remotely related, I'll place [Introduction to Formal Reasoning (COMP2065)](http://www.cs.nott.ac.uk/~psztxa/comp2065.23-24.ifr-notes/_build/html/index.html#) in this section so I won't lose track of it.
+}

trees/uts-001Y.tree

@@ -0,0 +1,23 @@
+\import{macros}
+
+\mdnote{Philosophy}{
+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](https://github.com/gjoncas/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 \citek{achourioti2011formalization} which might be interesting.
+}

trees/uts-001Z.tree

@@ -0,0 +1,41 @@
+\import{macros}
+
+\note{Generalized Clifford Algebra and related mathematical branches}{
+\md{
+A [Clifford algebra](https://en.wikipedia.org/wiki/Clifford_algebra) is a #{Z_2}-[graded algebra](https://en.wikipedia.org/wiki/Graded_algebra), and a [Filtered algebra](https://en.wikipedia.org/wiki/Filtered_algebra), the associated graded algebra is the [exterior algebra](https://en.wikipedia.org/wiki/Exterior_algebra).
+
+It may be thought of as quantizations (cf. quantum group) of the exterior algebra, in the same way that the Weyl algebra is a quantization of the symmetric algebra. [Specifically](https://ncatlab.org/nlab/show/Clifford+algebra#AsQuantizedExteriorAlgebra), for #{V} an inner product space, the symbol map constitutes an isomorphism of the underlying super vector spaces of the Clifford algebra with the exterior algebra on  #{V}, and one may understand the Clifford algebra as the quantization Grassmann algebra induced from the inner product regarded as an odd [symplectic form](https://ncatlab.org/nlab/show/symplectic+form).
+
+Weyl algebras and Clifford algebras admit a further structure of a [*-algebra](https://en.wikipedia.org/wiki/*-algebra), and can be unified as even and odd terms of a [superalgebra](https://en.wikipedia.org/wiki/Superalgebra), as discussed in [CCR and CAR algebras](https://en.wikipedia.org/wiki/CCR_and_CAR_algebras).
+
+A [Clifford module](https://en.wikipedia.org/wiki/Clifford_module) is a representation of a Clifford algebra.
+
+A [Generalized Clifford algebra (GCA)](https://en.wikipedia.org/wiki/Generalized_Clifford_algebra) can also refer to associative algebras that are constructed using forms of higher degree instead of quadratic forms, e.g.
+
+> For #{q_1, q_2, \ldots, q_m \in \mathbb{k}^*}, the generalized Clifford algebra #{C^{(n)}\left(q_1, q_2, \ldots, q_m\right)} is a unital associative algebra generated by #{e_1, e_2, \ldots, e_m} subject to the relations
+> ##{ e_i^n=q_i \mathbf{1}, \quad e_i e_j=\omega e_j e_i, \quad \forall j \lt i . }
+>
+> It is easy to see that #{C^{(n)}\left(q_1, q_2, \ldots, q_m\right)} is #{\mathbb{Z}_n}-graded where the degree of #{e_i} is #{\overline{1}}, the generator of #{\mathbb{Z}_n}. \citek{cheng2019new}
+
+In \citek{cheng2019new}, note also that "Clifford algebras are weak [Hopf algebras](https://en.wikipedia.org/wiki/Hopf_algebra) in some symmetric tensor categories." while "generalized Clifford algebras are weak Hopf algebras in some suitable braided linear categories of graded vector spaces." as well as that "the Clifford process is a powerful technique to construct larger dimensional Clifford algebras from known ones."
+
+TODO: add papers linking Hopf algebra and Clifford algebra together learned from the adjoint discord here.
+
+Clifford algebras can be obtained by twisting of group algebras \citek{albuquerque2002clifford}, where twisted group algebras are studied in \citek{conlon1964twisted}, \citek{edwards1969twisted}, \citek{edwards1969twisted2}.
+
+There exists isomorphisms between certain Clifford algebras and NDAs (Normed Division Algebras) over #{\mathbb{R}}.
+
+Variants of Clifford algebras whose generators are idempotent or nilpotent can be considered. Zeon algebras ("nil-Clifford algebras") have proven to be useful in enumeration problems on graphs where certain configurations are forbidden, such as in the enumeration of matchings and self-avoiding walks. The idempotent property of the generators of idem-Clifford algebras can be used to avoid redundant information when enumerating certain graph and hypergraph structures. See \citek{ewing2022zeon}.
+
+It's also closely related to universal enveloping algebra (see \citek{figueroa2010spin} and "The universal enveloping algebra of a Lie algebra is the analogue of the usual group algebra of a group." from [group algebra on nlab](https://ncatlab.org/nlab/show/group+algebra#RelationToUniversalEnvelopingAlgebra)).
+
+Great discussions about the limitations and generalizations of Clifford algebras can be found in John C. Baez's \citek{baez2002octonions}. Particularly, note [Cayley-Dickson construction](https://en.wikipedia.org/wiki/Cayley-Dickson_construction), Bott periodicity, matrix algebra, triality, and #{\mathbb{R}} as a real commutative associative nicely normed ∗-algebra. Also see Anthony Lasenby's work on the embedding of octonions in the Clifford geometric algebra for space-time STA ( #{\mathop{\mathcal{C}\ell}(1, 3)} ) \citek{lasenby2024some}.
+
+Note also Kingdon algebras: alternative Clifford-like algebras over vector spaces equipped with a symmetric bilinear form \citek{depies2024octonions}.
+}
+
+\transclude{uts-0020}
+\transclude{uts-0021}
+\transclude{uts-0022}
+\transclude{uts-0023}
+}