Simon DeDeo Assigned Three Research Projects to AI Agents
Simon DeDeo Assigned Three Research Projects to AI Agents
On August 1, researcher Simon DeDeo described a pilot study: three parallel runs of GPT 5.6-sol received his earlier papers, access to a 32-core machine, and access to Carnegie Mellon University's computing cluster. Within one or two days, the agents collected data, wrote programs, and prepared reports. Two of the projects can already be examined through public repositories.
DeDeo wanted to find out whether an agent could continue a line of research begun by a human. He gave each run a topic and source materials, then returned with questions and asked the agents to check their calculations and text again. One agent analyzed parliamentary speeches. Another examined formal proofs in Lean, a language in which a computer verifies every step. The third project concerns readers' notes.
The repository for the proof project contains a manuscript titled “Proofs for Now and Proofs for Later.” It compares 3 635 pairs of valid Lean proofs for the same propositions. Versions produced by the model more often contain intermediate statements with generic names such as h or step2. These statements are then referenced less often later in the proof.
A proof serves both the immediate task and the next reader. In a lecture on “proof digestion”, Terence Tao distinguished checking individual steps from the work through which a mathematician understands a method and connects it to the broader theory. The authors of DeDeo's manuscript call this second horizon “amortization”: a person can name a lemma so that it remains useful in the next step or in later work. They hypothesize that when the goal is simply to produce a finished answer, local statements are more likely to remain single-use. The matched pairs show differences in how such statements are named and whether they are referenced later.
The second public project contains the code, manuscript, and audit for an analysis of 1 643 387 speeches by legislators from 24 European parliamentary systems. Opposition speeches were statistically more likely to be novel than speeches from the governing coalition after speeches delivered on the same day were compared and the analysis accounted for the speaker, parliament, and year.
In the review guide, every central claim is linked to a script and an output file. The authors also list the preliminary claims they withdrew and explain the reason for each revision. A reviewer can follow the sequence from claim to computation, result, and correction, then decide where further work is needed.
The pilot provides a verifiable path from each claim to its computation and correction. The agent collects the data and performs the calculations, while the human frames the question and checks the chain of reasoning. Public scripts and revision records give the next researcher a specific point from which to continue the analysis.