Stanford researchers introduced CausalSmith, an agentic pipeline for automating theoretical research in causal inference. The system proposes results, checks them with a language-model reviewer, formalizes proofs in Lean 4, and produces papers with interactive web pages and slide decks. Its supporting Causalean library contains more than 15,000 Lean-verified definitions and theorems in statistics and causal inference.

CausalSmith runs through discovery, formalization, and presentation. During discovery, an agent proposes a result and writes a natural-language proof for review; another agent checks its correctness and novelty. Lean then checks the proof, while an audit compares each formal statement with the paper’s assumptions and conclusions to catch changes that could make a theorem weaker than claimed. The final stage creates a human-readable paper, an interactive page, and a 20-minute slide deck.

The researchers illustrate the process with a result on estimating the average treatment effect under discrete confounding. A 2024 paper by Zeng and colleagues established a lower bound but left open whether an estimator could reach it. CausalSmith proposed an estimator that closes the gap and achieves the minimax rate. To complete its Lean proof, the pipeline established concentration bounds for random counts that were missing from Mathlib, Lean’s standard math library, and added them to Causalean. The researchers say they manually checked the featured paper and found proof techniques not previously applied in causal inference.

As of October 2026, the team had run CausalSmith 1,732 times: 41 runs, or 2.4%, were accepted as correct, fully proved in Lean, and sufficiently novel under the review criteria set for each run. Another 1,388 were downgraded because reviewers considered their correct math incremental, and 303 failed after a proposal or its math was rejected. Accepted, downgraded, and failed runs are stored in a run bank so later runs can learn from earlier attempts. Reusable lemmas and theorems are generalized, reviewed, and added to Causalean; a later accepted result on the same problem reused the concentration bounds rather than proving them again.

Causalean was built because Mathlib contains almost no causal inference material. Researchers selected commonly used results from the literature, organized and formalized them with language-model assistance, and manually reviewed each statement. Later runs can add missing classical results after language-model review. The library covers causal graphs, potential outcomes, structural causal models, estimation, experiments, and panel data; reviewers also check that entries match their sources, are reusable, and are not vacuous. On the project page, readers can rate papers, comment on passages, certify individual statements, and compare many natural-language definitions and theorems with their audited Lean versions. Papers that pass novelty review and Lean verification receive a DOI and citation.

The researchers said they had manually reviewed only a small portion of the papers produced as of October 2026, so the overall quality remains unknown. For now, ratings, certifications, and comments on the project page are the main ways to gather human judgment. They identified more systematic novelty measures and a benchmark for evaluating language models’ ability to conduct novel research as future directions.

Stanford researchers introduced CausalSmith, an agentic pipeline for automating theoretical research in causal inference. The system proposes results, checks them with a language-model reviewer, formalizes proofs in Lean 4, and produces papers with interactive web pages and slide decks. Its supporting Causalean library contains more than 15,000 Lean-verified definitions and theorems in statistics and causal inference.

CausalSmith runs through discovery, formalization, and presentation. During discovery, an agent proposes a result and writes a natural-language proof for review; another agent checks its correctness and novelty. Lean then checks the proof, while an audit compares each formal statement with the paper’s assumptions and conclusions to catch changes that could make a theorem weaker than claimed. The final stage creates a human-readable paper, an interactive page, and a 20-minute slide deck.

The researchers illustrate the process with a result on estimating the average treatment effect under discrete confounding. A 2024 paper by Zeng and colleagues established a lower bound but left open whether an estimator could reach it. CausalSmith proposed an estimator that closes the gap and achieves the minimax rate. To complete its Lean proof, the pipeline established concentration bounds for random counts that were missing from Mathlib, Lean’s standard math library, and added them to Causalean. The researchers say they manually checked the featured paper and found proof techniques not previously applied in causal inference.

As of October 2026, the team had run CausalSmith 1,732 times: 41 runs, or 2.4%, were accepted as correct, fully proved in Lean, and sufficiently novel under the review criteria set for each run. Another 1,388 were downgraded because reviewers considered their correct math incremental, and 303 failed after a proposal or its math was rejected. Accepted, downgraded, and failed runs are stored in a run bank so later runs can learn from earlier attempts. Reusable lemmas and theorems are generalized, reviewed, and added to Causalean; a later accepted result on the same problem reused the concentration bounds rather than proving them again.

Causalean was built because Mathlib contains almost no causal inference material. Researchers selected commonly used results from the literature, organized and formalized them with language-model assistance, and manually reviewed each statement. Later runs can add missing classical results after language-model review. The library covers causal graphs, potential outcomes, structural causal models, estimation, experiments, and panel data; reviewers also check that entries match their sources, are reusable, and are not vacuous. On the project page, readers can rate papers, comment on passages, certify individual statements, and compare many natural-language definitions and theorems with their audited Lean versions. Papers that pass novelty review and Lean verification receive a DOI and citation.

The researchers said they had manually reviewed only a small portion of the papers produced as of October 2026, so the overall quality remains unknown. For now, ratings, certifications, and comments on the project page are the main ways to gather human judgment. They identified more systematic novelty measures and a benchmark for evaluating language models’ ability to conduct novel research as future directions.