A Summer with Claude and Relative Arbitrage, by Dmitriy Traytel

Dmitriy Traytel, working under a Renaissance Philanthropy-funded project on Copilots for Isabelle, used Anthropic's Claude models with Kevin Kappelmann's PIDE MCP component to autoformalize the main result of a not-yet-published paper on the relative arbitrage problem under eigenvalue lower bounds into a finished Isabelle/HOL proof in three weeks, producing over 100,000 lines of proof. Traytel ran Claude nearly non-stop on a Claude Max 5x subscription, with Claude Fable 5 drafting within its token limits and Claude Opus 5 (starting from Opus 4.8) taking over from the current proof state, notes and plans; the prompt was essentially "Formalize https://arxiv.org/abs/2512.17702 in Isabelle using PIDE MCP." The proof, covering Theorem 1.1 from the joint article by Misha Shkolnikov, Jou-Hua Lai and H. Mete Soner, is published at github.com/dtraytel/relative_arbitrage.

In our Renaissance Philanthropy-funded project Copilots for Isabelle https://www.renaissancephilanthropy.org/copilots-for-isabelle-learning-logical-structure-for-a-better-proving-experience , 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 https://github.com/kappelmann/isabelle-pide-mcp component<sup 1 fn:1 </sup , 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 https://www.math.cmu.edu/~mshkolni/ recently gave a talk at the Mathematics for the Real World 2026 https://www.sdu.dk/en/forskning/qm/events/icmu-conf-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 summer that Misha was coming to visit, I decided to prepare a surprise: I asked Claude to autoformalize, in Isabelle using PIDE MCP, the main result of his joint article with Jou-Hua Lai and H. Mete Soner not-yet-published, but in the final stages of the publication process on the Relative arbitrage problem under eigenvalue lower bounds https://arxiv.org/abs/2512.17702 . Mandatory note here: I am quite clueless about financial mathematics and probability theory in general, let alone stochastic portfolio theory and relative arbitrage: e.g., I learned from the article’s first sentence that Fernholz has introduced the concept of portfolio domination, now more commonly referred to as relative arbitrage, to rigorously capture the notion of “beating the market”. I picked this particular result for the aforementioned detachment reasons, but also because it scored highly along the “recent work”—”short proof” curve among Misha’s recent papers available on arXiv. Three weeks and over 100 000 lines later I had a finished Isabelle/HOL proof https://github.com/dtraytel/relative arbitrage . Claude was working nearly non-stop during these three weeks. I used a Claude Max 5x subscription over the summer, which has since been replaced by the Claude Team plan for scientists. The workflow was: Claude Fable 5 drafted as much as it could within its harsh token limits. When those were exhausted, Claude Opus 5 I may have started with Opus 4.8 took over based on the current proof state, notes, and plans that Fable developed. Generally, my prompt was more or less “Formalize https://arxiv.org/abs/2512.17702 in Isabelle using PIDE MCP” followed by numerous encouragements to keep going and occasional suggestions to look at the Archive of Formal Proofs before formalizing a new concept. I am in no position to discuss the mathematical aspects of this autoformalization, but I have something to say about the outcome and the challenges along the way which will include some mathematics in case you are here solely for that purpose . The main result, Theorem 1.1, itself has a rather complex statement. Here it is, with HTML generated from Isabelle while hiding comments . Feel free to skip it; there is not enough context given here anyway to understand it fully. I include it here for completeness and to give a flavor of how things look. theorem theorem 1 1: fixes K :: " real^'n::finite set" assumes kn: "k < CARD 'n " and L1: "1 ≤ L" and k1: "1 ≤ k" and cK: "compact K" defines "v ≡ λz. enn2real xval k L K z " shows " ∃B :: real. ∀y. xval k L K y ≤ ennreal B ∧ ∀c z. v z < c ⟶ ∃e 0. ∀y. dist z y < e ⟶ v y < c ∧ visc subsol env2 k L K interior K ∪ {x ∈ K - interior K. 0 < v x} v ∧ visc supersol env2 k L K interior K ∪ {x ∈ K - interior K. lsc envK K v x < 0} lsc envK K v ∧ expandable K ⟶ ∀u :: real^'n ⇒ real. ∀Bd. ∀c z. z ∈ K ⟶ u z < c ⟶ ∃e 0. ∀y∈K. dist z y < e ⟶ u y < c ⟶ ∀y∈K. ¦u y¦ ≤ Bd ⟶ visc subsol env2 k L K interior K ∪ {x ∈ K - interior K. 0 < u x} u ⟶ visc supersol env2 k L K interior K ∪ {x ∈ K - interior K. lsc envK K u x < 0} lsc envK K u ⟶ ∀x∈K. u x = v x " The formalization pulls in material from HOL-Analysis and HOL-Probability, but also six AFP entries: Disintegration, Kolmogorov Chentsov, Levy Prokhorov Metric, Lower Semicontinuous, Martingales, Standard Borel Spaces. I tasked Claude to explain the definitions that were introduced on top of these dependencies and to compare the statement to the one from the paper in a visual/interactive way. The output is available here https://lawrencecpaulson.github.io/assets/theorem 1 1 unfolded.html and I find it surprisingly readable in that it contextualizes things better than Isabelle’s unprocessed HTML output. I am particularly fond of the nested tooltips to explore definitions something I suggested to Claude —we need deterministic tools that generate such a presentation of formal material. Fortunately, Isabelle/PIDE has all the markup we need already, so this is really a question of presentation. The main question with any autoformalization is whether the theorem states the right result: I believe that it does after eyeballing the paper and the formal definitions. And after showing a more static PDF variant of the above document to Misha, the belief has only grown stronger. Needless to say, Isabelle checked the proofs, so fortunately I did not need to study those carefully. Claude’s original formulation was spread over five lemmas with different assumptions. Two interesting things happened: ∃B :: real. ∀y. enn2real xval k L K y ≤ B , which does not achieve the intention to state that xval never returns ∞ because the conversion enn2real from extended non-negative reals to reals assigns 0::real to ∞::ennreal in Isabelle a standard “totalization” completion xval k L K y is never ∞. It just managed to forget this when stating the final lemma. After realizing the issue, it was thus immediate to obtain the current formulation with the embedding of reals into extended non-negative reals on the right of the inequality. The first complete proof had over 100 000 lines, which sounds impressive by human standards. From the start, I doubted that it had to be that long. Restructuring eventually shrank it by about a third see below , although I never pushed very hard for really concise proofs. I did instruct the agents to iteratively remove lemmas that were flagged as unused when looking at the theorem dependencies unused thms . There were some in the end but not too many. Granted, the agents had to develop a lot of infrastructure that the authors assume to be pre-existing. And this is not counting advanced analysis and probability theory that was already in Isabelle and the AFP. On several occasions the authors’ proofs are of the form: “repeat the Larsson–Ruf argument word-by-word”, which required the agents to read more than the 17-page paper—so the de Bruijn factor may be smaller than it sounds. The proofs the agents write consist of rather small steps. Here are for example the five most frequently used proof methods along with the number of occurrences in the current formalization: 6736 rule 6469 simp 1621 intro 1318 blast 917 auto Of course, different authors have different proof styles. My typical proofs consist of more auto s and fewer rule s, here e.g., in VeriMon https://bitbucket.org/jshs/monpoly/src/master/thys/ 68 000 lines of Isabelle : 6962 auto 2502 simp 1259 cases 909 blast 890 rule Apart from the need to deal with huge amounts of formal material, having small-step proofs is not necessarily a bad thing. In fact, proof processing is very efficient: isabelle build including document preparation finishes in under five minutes on my machine. The first completed proof https://github.com/dtraytel/relative arbitrage/tree/af1bae57eacece10892a88759e9a4d2b86fee4e1 consisted of 64 theories dumped in a single session. I instructed the agents to separate generally reusable material from things that are specific to the proof and to use these abstractions and generalization to shrink the material. This exercise was repeated multiple times as new models would be released e.g., Claude Opus 5.5 . After these improvements, the formalization currently consists of only 85 000 lines structured in 12 sessions, of which 9 could become “library-style” AFP entries roughly 70 000 lines together , two formalize the main result 13 000 lines , and one presents the result in the paper’s notation 1 800 lines . I write “could” because it is not clear to me whether this material belongs to the AFP in the current form , and I fear that I might not have enough understanding of the material to bring it into the desired form. I welcome any contribution from experts on such material I’m thinking, e.g., of the authors of the entries the formalization uses , although I don’t want to force a formalization that may contain AI slop on anyone. I’m also trying to be conservative when it comes to AFP submissions because, as an AFP editor, I already see how much AI-generated material we are receiving—not all bad, but also by far not all good. Misha tells me that second-order viscosity analysis, in particular the Crandall–Ishii –Lions result, is a standard and widely used tool in stochastic optimal control. This makes me hopeful that the present autoformalization can be useful for future formalizations in this area. Perhaps the most human trait of LLM agents is their laziness. When making TODO lists, the agents will structure them in such a way that low-hanging fruit is handled first, creating an illusion of fast progress. An example is Crandall–Ishii, which the agents had enormous respect for and thus kept postponing. Eventually, there was no way around it, but amusingly the agents went for the bare minimum and formalized only the core argument needed for Theorem 1.1, not the full Crandall–Ishii theorem. After Misha told me about Crandall–Ishii’s importance, I instructed the agents explicitly to fill this gap. In other places, the laziness actually paid off. The agents managed to avoid formalizing stochastic integrals and Itô’s formula, both used in the paper. I cannot really say what they did instead and whether it was better, worse, or mathematically interesting . Claude has mixed feelings about this and justifies it with the claim that developing this “Itô-calculus” machinery, which Isabelle lacks, would be a substantial project. Technologically, PIDE MCP was the perfect interface for the autoformalization part of the job. The MCP server gave the agents up-to-date access to Isabelle’s feedback on their edits. People using agents with isabelle build frequently want to single out non-terminating commands by introducing timeouts. Every now and then agents would produce non-terminating proofs often when using blast , but PIDE MCP makes it easy for them to detect these issues by labeling the offending commands as “potentially non-terminating” whereas PIDE’s standard terminology is “running”, which has a positive connotation that may confuse agents: when something is running it is often a good thing . The later refactoring bits proved more challenging: dynamic handling of sessions was not yet supported by PIDE MCP at the time it is now , so every structure change required a restart of the MCP server and thus a restart of Claude Code . This formalization was an odd experience. I consider myself an experienced formalizer and for me, completing a formalization is always accompanied by a sense of accomplishment, ownership, and understanding: now I really know how it works These aspects were to a large degree absent here. Sure, in some sense it is satisfying to see the agents tick off boxes from their own TODO lists. But it is not the same as doing it oneself. Also, at times boxes get replaced by more boxes—a real Hydra fight typical of a large proof development—but without the understanding these boxes mean relatively little and one does not get a good grip on whether we are converging towards the goal or the agents just engage us in burning more tokens. The agents have mixed success when estimating difficulty and their own capabilities. In terms of learning how things work: I certainly learned some things while watching the agents work on the formalization: likely enough to understand the theorem statement, but not enough to distinguish which parts of the proof are reusable and which ones are specific to the theorem. Odd things also happen in the brains of these machines. I get particularly annoyed when the thinking trace is shown and I see “thoughts” like “Writing Lean proof.” or complaints like “nlinarith is not available in this version of Isabelle”. At no point did I catch the agents actually mistaking Lean’s syntax for Isabelle’s—these artifacts did not make it out of the “thoughts”—but they constitute a reminder that these machines may not be as intelligent as their proof assembly capabilities suggest. A point Larry will appreciate: even during thinking, none of the agents ever complained about Isabelle’s lack of dependent types https://lawrencecpaulson.github.io/2025/11/02/Why-not-dependent.html . Where does one go from here? It seems feasible to obtain formalizations of recent mathematical results with bounded resources.<sup 2 fn:2 </sup Looking at the cost question in more detail, the subscription cost of $100 monthly must be contrasted with the much higher calculated API cost: Claude estimates $7 500, with roughly 9.7 billion input tokens and 20 million output tokens distributed over 30% Fable and 70% Opus the same distribution is observed when attributing Isabelle lines to models that produced them —here we are not counting the cleanup and restructuring that followed the first proved version of Theorem 1.1. Which results should we focus on for this price? Many formalizers will care about the structure of the proof. The particular exercise seems to have been useful to Misha to straighten out the L = 1 case, regardless of the formalized proof structure. From the proof assistant perspective it is also interesting to compare technologies and libraries. Would it be cheaper, for instance, to autoformalize the same result in Lean? Also better tool support, especially for refactoring and making sense of definitions and statements, is dearly needed. I included some critical thoughts above, but want to end on a positive note: the paradigm shift that these funny machines bring to proof assistants makes the work of our community more relevant than ever: formal proofs will be everywhere and easy to generate, also by non-experts. We just need good tools for inspecting and assessing the quality of the results and an army of domain experts to sieve through the mud and find the gold nuggets. Acknowledgements . Thanks to Mohammad Abdulaziz, David Basin, Kevin Kappelmann, and Misha Shkolnikov for comments on earlier drafts of this article. Another useful MCP for Isabelle is I/Q https://github.com/awslabs/AutoCorrode/tree/main/iq . Have a look at the PIDE MCP preprint https://zenodo.org/records/21519365 for an architectural comparison of PIDE MCP, I/Q, and other viable approaches connecting agents to Isabelle. ↩ fnref:1 Since this summer, big tech companies have showcased that with unreasonable amounts of resources and in part using internal, unpublished models one can jump even higher and run even faster. Here, I report on using the technology they make available to ordinary subscribers. ↩ fnref:2