Iowa Type Theory Commute

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

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.