# CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference

arXiv: https://arxiv.org/abs/2607.22511 · HTML: https://mlsanity.com/paper/2607.22511/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Medical and scientific domain agents, one of 16 directions in LLM agents and tool use.
- Builds on 50 of its 62 references that are in the map.
- First posted on arXiv 24 Jul 2026.

## Placed in

- LLM agents and tool use / [Medical and scientific domain agents](https://mlsanity.com/agents/medical-and-scientific-domain-agents/)
- Synthetic data and self-improvement for LLMs / [Self-evolving LLM agents](https://mlsanity.com/synth/self-evolving-llm-agents/)

## Builds on (most cited first, 30 of 50)

- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search](https://mlsanity.com/paper/2504.08066/) (2025)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Causal Reasoning and Large Language Models: Opening a New Frontier for Causality](https://mlsanity.com/paper/2305.00050/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Causal Parrots: Large Language Models May Talk Causality But Are Not Causal](https://mlsanity.com/paper/2308.13067/) (2023)
- [Can Large Language Models Infer Causation from Correlation?](https://mlsanity.com/paper/2306.05836/) (2023)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [CLadder: Assessing Causal Reasoning in Language Models](https://mlsanity.com/paper/2312.04350/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Is ChatGPT a Good Causal Reasoner? A Comprehensive Evaluation](https://mlsanity.com/paper/2305.07375/) (2023)
- [Are LLMs Capable of Data-based Statistical and Causal Reasoning? Benchmarking Advanced Quantitative Reasoning with Data](https://mlsanity.com/paper/2402.17644/) (2024)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [Causal Inference with Large Language Model: A Survey](https://mlsanity.com/paper/2409.09822/) (2024)
- [Evaluating Sakana's AI Scientist: Bold Claims, Mixed Results, and a Promising Future?](https://mlsanity.com/paper/2502.14297/) (2025)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [LLMs Are Prone to Fallacies in Causal Inference](https://mlsanity.com/paper/2406.12158/) (2024)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [Causal Evaluation of Language Models](https://mlsanity.com/paper/2405.00622/) (2024)
- [Causal-Copilot: An Autonomous Causal Analysis Agent](https://mlsanity.com/paper/2504.13263/) (2025)

## Built on by (most cited first, 1 of 1)

- [Counterfactual Predictions in Scientific Emulators Without Controlled Experiments](https://mlsanity.com/paper/2610.02252/) (2026)

## Abstract (arXiv)

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~citepbadscientist2025. We present textscCausalSmith, 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. textscCausalSmith rests on textscCausalean, 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.