• First-Derivative Test (2024, with Patrick Massot and Floris van Doorn)
• Equivalence between one-point compactification of $\mathbb R$ and the projective line (2024, with Oliver Nash)

• Marginis – formalia marginalia for the Journal of Logic and Analysis
• Protein folding – formalizations related to the paper Nonmonotonicity of protein folding under concatenation
• Automatic complexity – formalized exercise solutions for my book
• Dyadic deontic logic – formalized results from a paper in preparation (with Rachelle Edwards)
• Jaccard – formalization research paper Interpolating between the Jaccard distance and an analogue of the normalized information distance (Journal of Logic and Computation, 2022)

My book “Automatic complexity: a computable measure of irregularity” was published by de Gruyter on February 19, 2024. It concerns a version of Sipser’s complexity of distinguishing that was introduced by Shallit and Wang in 2001 and has been developed by me and others since 2013.

Erratum

Theorem 6.6: Two constructions $M_1\times_1 M_2$ and $M_1\times_2 M_2$ are described. The text suggests that $\times_1$ is used for the theorem, but actually $\times_2$ should be used. The operation $\times_1$ can be used to prove the inequality $A_N(x)\le A_N(x\mid y)\cdot A_N(y)$ instead.