I was discussing two-column proof with some colleagues today and I mentioned how it reminds me a bit of the formalization movement in , like proof checkers and theorem provers. "Do you mean like Lean?" my colleague asked. "Yes," I said. She got very excited: "Kevin Buzzard was my professor!" @xenaproject@mathstodon.xyz