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

TL;DR - CausalForge is an agentic framework for automated causal-inference research that uses Lean to verify proofs. It addresses unreliable LLM review by combining kernel-checked formal verification with audits linking formal theorems to their intended scientific claims.

• Causalean provides 7,035 machine-checked causal-inference declarations developed with LLM assistance and human oversight.
• CausalSmith autonomously selects topics, proposes results, formalizes statements, constructs proofs, and produces artifacts for human inspection.
• Statement audits check whether each formal theorem faithfully represents its corresponding informal claim.
• The evaluation uses artifacts from completed autonomous research runs; code, formal libraries, and run records are publicly available.