Post by @tao@mathstodon.xyz

2026-06-21 17:53 UTC

&quot;I have only made this letter longer because I have not had the time to make it shorter.&quot; (Blaise Pascal, often misattributed to Mark Twain) I have previously written about the evolving impedance mismatch between proof generation, proof verification, and proof digestion in mathematics. This has led to the following unintuitive breakdown of monotonicity, already noticed by Pascal as far back as 1657: it is now easier to generate long correct proofs than it is to generate short correct proofs! However, it is far more challenging to *verify* and *digest* such proofs, thus exacerbating the impedance mismatch. I have encountered this phenomenon personally with the Integrated Explicit Analytic Number Theory Network (IEANTN) project https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/ . As part of this project, a large number of lengthy technical papers in explicit analytic number theory are to be formalized. This was a tedious task, involving a lot of numerical verifications, and until recently was the bottleneck for the project; I could assign individual lemmas to formalize as tasks, and expect it to take weeks before a volunteer would claim them and prove them. Because the task of formalization by hand was difficult, the volunteer would naturally strive to make the proofs short, efficient, and natural, and as such they were easy to review by myself. (1/3)

Replies (2)

@tao@mathstodon.xyz 2026-06-21 17:53

In the last few weeks, though, autoformalization has reached the point where virtually every formalization task I had issued could be completed within hours. However, the formalization tools tended to create quite bloated proofs, often hundreds of lines longer than what a human would choose to do, with a lot of redundancy, with many lemmas not stated at the natural level of abstraction. For any individual result, this is not a major problem - the proofs here are not intended to be read by humans anyway, but because each such proof adds tens of seconds to the total build time, the cumulative effect of such large AI-generated proofs has become noticeable, and somewhat difficult to review. In particular, the process of converting a medium-sized Lean document (containing a few thousand lines of code, with some proofs AI-generated) into a nicely golfed and structured Mathlib submission has been an interesting experience. AI agents can be used to perform local golfs that can shave the size of the code somewhat, but global refactoring decisions, such as noticing that a certain argument appears multiple times across the document and can be abstracted into a standalone lemma that can may have additional utility beyond the file, is still largely beyond the reach of current AI tools. (I find that I can *explain* such a refactor to an AI agent, who can then execute it, but they struggle to spontaneously *discover* such refactors on their own.) (2/3)

Open ##5165524
@fckprknsns@mathstodon.xyz 2026-06-22 07:18

@tao@mathstodon.xyz Is it possible to somehow not only verify a proof but also to verify that a correct proof is the shortest possible proof of that statement?

Open ##5165528