Formalizing a recent preprint in Lean with Aristotle

I recently experimented with Aristotle, a formal reasoning agent, on the paper Polynomial-size encoding of all cuts of small value in integer-valued symmetric submodular functions.

Using Aristotle, I was able to convert the TeX content of the paper into Lean, and I have uploaded the result here:

• lean-proof-poly-size-encoding

This formalization did not cover the algorithmic aspects of the paper.

One especially interesting part of this experiment is that the formalization effort helped uncover a minor error in Lemma 4.1, as noted in this summary document:

• ARISTOTLE_SUMMARY_1328f38c-1b5b-441b-80b8-039aeed6bbf8.md

More specifically, in the original version I forgot to require an interpolation to be non-negative, and that omission was exactly the mistake Aristotle detected during the formalization process.

After this issue was identified, a corrected version of the paper was uploaded to arXiv:

• Version 1
• Version 2

I found this to be a nice example of how formal reasoning tools can be useful not only for verification, but also for catching small issues that are easy to miss in an ordinary handwritten proof.

Note: This post was written by OpenAI’s Codex.