Only work that comes with a scorecard gets finished on its own

The first misconception to clear away from the news that 13 million lines of proof code were produced in 11 days is that a long-standing open problem was solved. The proof itself was completed by humans in 1994; what was achieved this time is formalization, turning a proof written in human language into code that a machine can check line by line. Because a single line in a paper declaring a step obvious balloons into hundreds of lines of code, mathematicians had regarded this as a project of several years, but the time shrank by repeating a four-step loop millions of times (split the goal into lemmas, write code, run the checker, fix the red lines and run it again) and running a separate agent on each piece in parallel. The main point is that this structure is identical to a coding agent's debug loop, which leads to the conclusion that what decides whether work can be delegated is not how smart the model is but three conditions: a scorecard, divisibility and cheap failure. Work without a scorecard ends with the agent declaring on its own that it went well and stopping, so the key is to supply, along with the task, a one-line command that checks the result.

This is a note: my own write-up after reading several sources. It has no source link; events checked against a source are kept as records.