Autonomous AI Agents Systematically Diverge From Human Preferences in Proof Formalization
Bálint Gyevnár, Simon DeDeo
cs.AI
Nov 4, 2026 · v1
cs.HC
TL;DR
Replays commit histories of nine Lean formalization repositories, comparing AI coding agents' edit choices with human edits using syntactic, dependency-graph, and surprise features.
Abstract
Artificial intelligence (AI) systems have ushered in a new age of proof abundance, but helping humans understand these proofs requires new attention to the differences in how AI agents and humans pursue a proof-making task. We present "simulated collaboration", a methodology that allows us to examine two key questions: (1) the relative attention AI agents pay to surface syntax or, conversely, deeper underlying semantics, and (2) how and where AI agent preferences for what to do next diverge from human preferences. On a set of nine major human collaborations in Lean with 4.7M definitions across more than 6K commits, we find that, over the course of proof construction, AI agents (1) are far more strongly drawn than humans to explicitly marked gaps; (2) show a relative aversion to densely connected proof centers and to complex or surprising proof goals; and (3) are relatively attracted to surprising proof bodies, which they tend to regularize toward baseline. Our results highlight important blind spots and potential interventions for future human-AI collaboration in mathematics.
Problem
AI systems increasingly produce formal proofs, but little is known about how AI agents' choices during proof construction differ from those of human collaborators, or whether those choices support human understanding.
Approach
The authors introduce "simulated collaboration": at each human commit in nine major Lean formalization projects (e.g., FLT, PFR, sphere packing, PDL), Claude Code, Codex, and Gemini CLI are asked to take the next step from the human parent commit. Edits are characterized by syntactic features (sorry markers, length), semantic network position in a lexically parsed dependency graph, and per-token surprise of signatures and bodies measured with Lean provers (DeepSeek-Prover-V2, Goedel-Prover-V2, Kimina-Prover). Logistic regressions then compare which definitions each actor chooses to edit.
Results
Across 4.7M definitions and more than 6K commits, at least 59% of each agent's modifications touch definitions containing sorry, compared with about a fifth of human modifications. Agents avoid densely connected proof centers and surprising signatures, are drawn to surprising bodies, and push body surprise down toward baseline. The dataset and code are publicly released.
| Actor | Added % | Modified % | Removed % |
|---|
| Human | 0.90 | 0.59 | 0.41 |
| Claude | 0.39 | 0.52 | 0.03 |
| Gemini | 0.17 | 0.42 | 0.05 |
| Codex | 0.17 | 0.12 | 0.00 |
Share of definitions added and modified per actor (aggregated over all commits)
