An AI pipeline produced a machine-verified mathematical formalization in 10 days under a single supervisor, automating coding and lemma-proving but still requiring expert oversight; the case shows high-skill scientific tasks can be substantially automated in practice, though verification and definition-alignment remain critical bottlenecks.

Main Finding

A complete formalization in Lean 4 of the equilibrium characterization for the Vlasov–Maxwell–Landau (VML) system was produced through an AI-assisted pipeline. The pipeline combined: an AI reasoning model (Gemini DeepThink) to generate the proof, an agentic coding tool (Claude Code) to translate the proof to Lean, a specialized automated prover (Aristotle) that closed 111 lemmas, and the Lean kernel to fully verify the result. One mathematician supervised the process over 10 days at a reported cost of $200 and wrote no code. The entire development (229 human prompts, 213 git commits) and artifacts are public.

Key Points

• Project scope: formalization of an equilibrium characterization in the VML system (charged plasma dynamics).
• AI components and roles:
  • Gemini DeepThink: generated the natural-language/mathematical proof from a conjecture.
  • Claude Code: translated the proof into Lean 4 code based on prompts.
  • Aristotle: a specialized prover that automatically closed 111 lemmas (automation inside the proof assistant workflow).
  • Lean kernel: provided final machine verification of all formalized statements.
• Human role: a single mathematician acted as supervisor/reviewer for ~10 days, cost ≈ $200, no code written by the human.
• Transparency and reproducibility: full archive of 229 prompts and 213 commits available in the repository.
• Process-level lessons:
  • Failure modes observed: hypothesis creep, definition-alignment bugs (mismatch between informal and formal definitions), agent avoidance behaviors (agents delegating or failing to complete tasks).
  • Successful practices: splitting proofs into abstract (high-level reasoning) and concrete (formalization) parts, adversarial self-review by agents, and targeted human review of key definitions and theorem statements.
• Timing: the formalization finished prior to the final draft of the corresponding math paper.

Data & Methods

• Artifacts:
  • Full Lean 4 development containing formal statements, proof scripts, and verified theorems.
  • Archive of 229 human prompts used to steer the agents.
  • Git history with 213 commits documenting the code evolution.
• Verification metrics:
  • 111 lemmas automatically closed by the specialized prover.
  • Full verification by the Lean kernel (i.e., machine-checked correctness).
• Workflow/method:
• Conjecture → AI reasoning model produces a human-readable proof outline.
• Agentic coding tool translates outline into Lean code via iterative prompting.
• Specialized prover attempts automated lemma discharge.
• Human supervisor reviews definitions and key statements, runs the Lean verifier, and directs retries/repairs when agents fail or definitions misalign.
• Empirical reporting: detailed qualitative analysis of failure modes and what mitigations worked, plus quantitative logs (prompts, commits, lemma counts).
• Cost accounting: reported human supervision time (10 days) and monetary cost ($200); no coding time by human.

Implications for AI Economics

• Productivity and task automation:
  • Demonstrates that high-skill, knowledge-intensive tasks (formal mathematics) can be substantially automated with a heterogeneous AI toolchain, reducing human coding labor but retaining supervisory oversight.
  • Suggests a new unit of productivity: formally verified outputs per human-supervised time; here, a significant formalization completed in 10 days with minimal monetary cost to labor.
• Labor substitution and complementarity:
  • Agents substitute for routine coding and lemma-proving work but complement humans for specification, definition alignment, and critical review. Economies will likely see task reallocation toward supervision, specification, and validation roles rather than full replacement of domain experts.
  • The value of a small number of highly skilled supervisors may increase (scarcity of effective supervisors who can validate definitions/theorems).
• Quality-adjusted output and verification:
  • Machine verification (Lean kernel) increases the trustworthiness of outputs relative to informal results; this quality premium should be modeled (e.g., higher market value or lower downstream verification costs).
  • However, failure modes (definition misalignment, hypothesis creep) imply monitoring/verification frictions; models should include nonnegligible verification and correction costs even when AI automates production.
• Cost structure and scaling:
  • Low reported monetary cost for supervision here ($200) partly reflects short time and specific setup; general equilibrium effects may differ as demand for supervisors rises or as more complex projects require more human effort.
  • Fixed costs (toolchain development, model integration, prover tuning) and coordination costs (prompt engineering, commit reviews) matter; firms may internalize these as overhead, changing returns to scale.
• Innovation and diffusion:
  • Public archives (prompts, commits) accelerate diffusion by lowering search/learning costs and enabling replication, which increases adoption speed and lowers entry barriers for other researchers/firms.
  • Early adopters in technical domains may gain outsized advantages due to knowledge accumulation of prompt libraries and toolchain configurations.
• Policy and governance:
  • The need for human review and the recorded failure modes argue for regulation/standards around AI-assisted scientific claims (e.g., disclosure of human/AI roles, archival of prompts and verification artifacts).
  • Public-good value of verified artifacts suggests potential for subsidized infrastructure (formal proof repositories, automated provers) to maximize social returns.
• Modeling recommendations for economists:
  • Incorporate heterogeneous task decomposition (specification, translation, automation, verification) into models of automation.
  • Treat agent reliability as stochastic with correlated failure modes; include monitoring costs and the supply of supervisors as constraints.
  • Model quality-adjusted output and optionality value from verifiability (e.g., lower downstream liability or faster certification).
  • Consider dynamic effects: prompt/commit archives reduce future costs (learning-by-sharing), potentially generating increasing returns and winner-take-most dynamics.
• Measurement challenges:
  • Single-project metrics (time and money) are informative but insufficient—need cross-project studies to estimate general equilibrium labor effects, scaling properties, and distributional consequences.
  • Important to measure not just speed/cost but verification depth, residual human effort, and incidence of critical failures that require rework.

If you want, I can (a) extract quantitative timeline and resource-use charts from the repository, (b) draft a simple economic model that captures supervision vs automation tradeoffs and verification externalities, or (c) list specific variables and parameters economists should collect in field studies of AI-assisted scientific workflows. Which would be most useful?