As of this part, I didn’t take detailed notes from time to time. In fact, I wasn’t sure where this project was going. As I said, in writing mathematical posts, I was hard to please. I wanted a more succinct, readable, and precise source, which Markdown was not. And I wanted typography features, which Markdown couldn’t express.
Let me recount these considerations, to recapitulate and partly to organize my own thought. The easiest choice was just sticking to Mathjax in Markdown. However, one had to use Javascript preprocessing to effectively introduce macros, which wasn’t flexible. Some characters, such as < and >, conflicted HTML, and there were no unicode characters beyond those in standard LaTeX. Moreover, the latest version didn’t break long expressions.
Or it seemed to be the best that I abandon Jekyll altogether and write a equivalent system, which I might not be capable of.
I could use CSS to typeset fractions, vectors, and matrices, and \mathfrak, \mathbb, \mathcal, and \mathscr could be simulated by different fonts. Most symbols used in math weren’t encoded in prevalent unicode blocks, but Noto Symbol font might have them. Superscripts and subscripts were inherent in HTML, though recursive applications might not look nice. For example, a double superscript was traditionally smaller than a single superscript, which probably had to be specified by a CSS class. These tasks sounded possible, but not easy. There were other options, after extensive search, such as invoking MathML or save everything as images. Quickly I realized that directly inputting MathML was highly verbose. Saving images in the repository would soon reach the limit of Github page, which is \(1\) GB.
Lastly, for some time, perhaps by middle of December 2020, I actually considered completely abandoning traditional mathematical notation, and I entertained the possibility of designing a new language expressed entirely in ASCII characters. The symbols +, -, *, /, ^ continue to mean basic operations, and more complicated ones were to be represented by words integration, differentiation, as in Mathematica. The downside was that I wouldn’t be able to communicate with other people without additional effort. Even if I linked every post to a summary of convention, the probability that people managed to finish a post was diminishing.
Largely inspired by such contemplation on mathematical notation, between these months I kept wondering what an ideal proof presentation would be. I had the independent awareness that the traditional style of proof was in many ways inadequate. About the middle of August, I came across the Wikipedia post of Curry-Howard isomorphism, and that truly changed my worldview1 I searched widely to learn more about logic, mathematical foundation, intuitionistic mathematics, constructivism, type theory, and interactive theorem provers. Since this narrative isn’t centered about, so to say, these sorts of new mathematics, I would continue my train of thought without explaining these fancy terms.
In short, I had the urge to present classical mathematics in a more constructive manner. A thorough approach might be designing a pseudo code for a proof assistant, such as Coq, so that besides checking mentally as we usually did, it was easy to rewrite the presentation in a way it could be checked via Coq too. By the way, it was perhaps more aesthetically appealing to me to have a syntax comprising only of ASCII.
January, February, and March soon passed, and it occurred to me instead that classical mathematics was mostly fine, if few little changes were made. Just to be sure that I wasn’t missing much, I took a look at several proposed mathematical foundation, such as the introduction and appendix of homotopy type theory, and the original papers of calculus of constructions. Most importantly, my suggestion was that statements which weren’t identity nor partial orders, shouldn’t be buried in paragraphs, but should occupy a lone line and be numbered as equations. Moreover, the reasons of a proposition should go just above the equation, and that these reasons should be ordered according to the order of substitution. Finally, application of law of excluded middle and nonconstructive axiom of choice should be announced every time. These conventions could make it easier to recover the Curry-Howard isomorphism.
A balance between constructive inclination and tradition did appear to be feasible, making the scope of my project more reasonable.
It simply remains to design a markup which describes normal text and mathematics, and outputs HTML. This markup, as Markdown does, distinguishes italic and bold texts, and so on. Moreover, there has to be a mark which denotes the beginning and end of a math mode, so I’m free to rename the symbols as I wish. The code in the math mode, in turn, is to be converted to standard LaTeX. I’m ready to code.
❧ June 23, 2021
References
❉ T Coquand and G Huet, ‹The Calculus of Constructions›. «Information and Computation», 1988
❉ M H Sørensen and P Urzyczyn, «Lectures on the Curry-Howard Isomorphism». Elsevier, 2006
❉ V Voevodsky et al, «Homotopy Type Theory»
❉ Coq, ‹Typing Rules›