A Summer with Claude and Relative Arbitrage, by Dmitriy Traytel

In our Renaissance Philanthropy-funded project Copilots for Isabelle, we develop methods and tools that allow AI agents to conveniently interface with Isabelle. One major outcome of the project so far is Kevin Kappelmann’s PIDE MCP component1, which presents AI agents with a live view of Isabelle much like we human users have it through Isabelle/jEdit. I am trying to keep Claude entertained through ((semi-)auto-)formalization case studies using this tool; this was also the goal for my summer vacation (with a week of FLoC in the middle) where I was looking for a larger project on which Claude could work rather independently for a longer period of time. And one I would be reasonably detached from, so that I would not have the urge to check on the agent every hour. My second cousin Misha Shkolnikov recently gave a talk at the Mathematics for the Real World 2026 conference. On his way to Odense, he stopped in Copenhagen so that I could give him a small tour of the city. Knowing before the…