By the way, I'd like to note that it will likely be a formalization of not the last result in that conversation, but of one of the initial proofs that relied on the Langford sequences and theorems of their existence.