CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
Jiyuan Tan, Vasilis Syrgkanis
stat.ML
Jul 24, 2026 · v4
cs.AI cs.LG econ.EM
TL;DR
Builds Causalean, a Lean 4 library of about 7,000 causal-inference declarations, and an agentic pipeline that formalizes and proves new results in Lean 4.
Abstract
Automating theoretical research requires generating candidate results and evaluating them reliably. Models keep getting better at the first, while the second remains hard. A common approach asks one large language model (LLM) to review what another produced, yet such reviewers are empirically unreliable: they may accept fabricated papers and catch the fabrication at close to chance rates \citep{badscientist2025}. We present CausalSmith, a framework for automated theoretical research in causal inference built on the Lean proof assistant, where a proof is checked by a program rather than read by a referee. CausalSmith rests on Causalean, a foundational Lean library for causal inference holding 8,179 machine-checked definitions and theorems, developed with language-model assistance under human design and review. Around it, we build a self-improving agentic pipeline that selects research topics, proposes results, formalizes statements, constructs proofs, and presents the resulting artifacts for human inspection. Moreover, the pipeline pairs Lean verification with a statement audit that compares each formal theorem against the informal claim behind it. We evaluate the system using artifacts produced by completed autonomous research runs. The source code, formal library, and run records are available at
https://github.com/Jiyuan-Tan/CausalSmith.
Problem
Automated theoretical research needs reliable evaluation of candidate results, and LLM reviewers have been shown to be unreliable. Formal verification can certify proofs, but it is costly from first principles and does not guarantee that a formal statement matches the intended claim.
Approach
The authors built Causalean, a Lean 4 library of causal inference covering SCMs, potential outcomes, estimation, panel methods and causal discovery. It was developed with LLM assistance under human design and review. Around it, CausalSmith is an agentic state-machine pipeline with four stages: discovery, formalization, proof construction and presentation. A logic graph links informal claims to Lean declarations, and a statement audit checks each formal node against its intended claim and screens for vacuity and forbidden shortcuts (axioms, sorry, native_decide). Reusable lemmas from completed runs are promoted back into the library after human review.
Results
The library snapshot contains 7,035 declarations across 973 files and about 262k lines. Of 123 recorded autonomous runs, 9 produced accepted results that were sound, novel at the requested tier and fully proved in Lean 4. Another 44 were downgraded and 70 failed, for a 7% overall acceptance rate. Novelty ratings come from LLM judgments and were not validated by independent human evaluation.
| Disposition | Runs | Gate |
|---|
| Accepted | 9 | sound, novel at tier, proved in Lean 4 |
| Downgraded | 44 | sound, below novelty target |
| Failed | 70 | rejected at proposal or mathematics |
| Total | 123 | |
Run catalogue by disposition
