• 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. The book’s exercises have formalized solutions in the proof assistant Lean.

Errata

1. Exercise 1.12: the word “no” should be removed.
2. Theorem 1.41 (3) refers the reader to Chapter 2 for the function $A_N$. In fact, $A_N$ is introduced in Definition 1.21.
3. Claim 4.43: $b’\in\Sigma\setminus\{w_1,\dots,w_s\}$ should (obviously) be replaced by $b’\in\Sigma\setminus\{b_1,\dots,b_s\}$.
4. Theorem 4.49: The text claims
   

   Our witnesses for $A^{\mathrm{perm}}(x)\le |x|+1$ are doubly transitive since the generated group is $S_n$.

   However, the generated group is not $S_n$ in general. A minimal counterexample is the witness for the word $00$, which generates the group $\mathbb Z/3\mathbb Z \ne S_3$. Therefore, whether $A^{\mathrm{tra2}} \le A^{\mathrm{perm}}$ should be considered open. Python calculations suggest it is true for binary words $w$ with $|w|\le 4$, and for 00000, at least.

5. 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.