CausalForge Pairs AI Research Agents With Machine-Checked Causal Proofs
Researchers Jiyuan Tan and Vasilis Syrgkanis submitted CausalForge on July 24, combining a 7,035-declaration Lean library for causal inference with an agentic pipeline that proposes and formally verifies research results. The preprint and released code show how proof checking can constrain automated research, while also warning that a valid formal proof does not guarantee the formal statement matches the intended scientific claim.
Researchers Jiyuan Tan and Vasilis Syrgkanis submitted CausalForge on July 24, presenting a system that combines automated research agents with machine-checked causal-inference proofs. The work is available as an arXiv preprint, and the authors released the Lean library, agent pipeline and run artifacts in a public GitHub repository.
Two layers: Causalean and CausalSmith
CausalForge has two main components. Causalean is a Lean 4 library covering causal models, do-calculus, potential outcomes, identification methods and related statistical foundations. The authors report 7,035 machine-checked declarations developed with language-model assistance under human design and review.
CausalSmith sits above that library. It selects research topics, proposes results, translates claims into formal statements, constructs proofs and presents the resulting artifacts for human inspection. The public repository separates the foundational library from the theorem-generation pipeline so that Causalean does not depend on generated research outputs.
Proof checking is not the same as scientific validity
The paper makes an important distinction: Lean can verify that a theorem follows from its stated assumptions, but it cannot by itself confirm that the formal theorem faithfully represents the intended informal scientific claim. CausalForge therefore adds a statement-audit step that compares each formal result with the claim it is meant to express.
That design narrows one familiar failure mode in autonomous research. A language model cannot simply declare a proof valid when the proof assistant rejects it. But formal verification does not resolve questionable assumptions, poor problem selection or a mismatch between mathematical formalization and the real-world causal question.
What practitioners should take from it
For data scientists, the release is most useful as an architecture pattern: separate proposal generation, retrieval, formalization, kernel verification and human inspection into auditable stages. The repository also exposes source code and completed-run records, making the authors' workflow more inspectable than a paper-only system.
The results should still be treated as preprint findings rather than independently validated performance. The paper was newly submitted to arXiv, and the retrieved evidence consists of the authors' paper and their own released implementation. External review and reproduction will determine how reliably the approach transfers beyond the included causal-inference artifacts.
Key Points
- 1CausalForge combines a Lean causal-inference library with an agentic pipeline for proposing and formally verifying research results.
- 2The authors report 7,035 machine-checked declarations in the Causalean library.
- 3A separate statement audit addresses the gap between a formally valid theorem and the intended scientific claim.
- 4The paper is a new preprint, and the released implementation has not yet been independently validated in the retrieved evidence.
Scoring Rationale
The work offers a concrete, inspectable architecture for combining research agents with formal verification and is directly relevant to causal-inference practitioners. It remains an author-reported preprint without retrieved independent evaluation, which limits the certainty and immediate production impact.
Sources
Primary source and supporting public references used for this report.
Practice interview problems based on real data
1,625 SQL & Python problems across 15 industry datasets — the exact type of data you work with.
Try 250 free problems
