I start discussing this great paper by Dunfield and Krishnaswami, about how to extend a particular approach to type inference to handle polymorphism.

In this episode, I reflect on the recent announcement that Anthropic researchers have autoformalized the proof of Fermat's Last Theorem. That is, they instructed an LLM to create a computer-checkable proof, in the Lean prover, of this theorem, following existing paper proofs in the literature. The resulting proof weighs in at 13 million lines of Lean, a staggering amount.

I talk about my efforts to formalize lambda-calculus with named variables and explicit alpha-equivalence, as originally proposed by Church. One reason to do that, besides just a love of being ornery, is to be able to state and prove theorems about alpha-equivalence. One example class of such theorems concern when alpha-equivalence can be avoided, in the sense that beta-reduction can proceed without any variable capture, while not requiring renaming variables. I have a companion blog post that talks about this, with a link to the repo with my Agda code so far.

A system of word equations is called quadratic if no variable occurs more than twice in it. There is an interesting simple algorithm to solve quadratic systems of word equations, which I talk through in this episode. My source is Chapter 12 of "Algebraic Combinatorics on Words" by Lothaire.

The problem of word equations is a rather storied one, including frustrated connections to Hilbert's Tenth problem. Word equations relate expressions consisting of concatenations of variables and constant symbols. An example is a X = X a, where X is a variable and a is a constant. A solution maps variables to strings of constant symbols making the two sides identical. In this episode, I discuss the problem a little, and what I learned so far about how it is solved.

In this episode, I give further arguments in favor of coercive subtyping from a software-engineering perspective. I also explain the critical concept of coherence.

I explain the story from last episode.

The Curry-Howard isomorphism for the law of excluded middle, as a radio drama. I first saw a version of this story performed by Phil Wadler and Frank Pfenning (wearing fake horns!) at RTA in Nara, Japan in 2005. This is my take on it. In a subsequent episode, I will explain how the story illustrates the computational interpretation of the law of excluded middle.