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

CausalForge presents an automated research framework for causal inference grounded in the Lean proof assistant. It combines Causalean, a foundational library containing 7,035 machine-checked declarations, with CausalSmith, an agentic pipeline that selects topics, proposes results, formalizes statements, constructs proofs, and prepares artifacts for human inspection. The authors distinguish kernel verification from scientific validity: a proof confirms that a formal theorem follows from its assumptions, but not that the theorem correctly represents the intended claim. A separate statement-audit stage addresses that gap. Source code, the formal library, and run records are released on GitHub.