Overview
Automating theoretical research is constrained not only by the generation of candidate results, but also by their reliable evaluation. A common approach is to close the research loop with a large language model (LLM) reviewer. However, such reviewers remain empirically unreliable: they may accept fabricated papers and detect them at rates close to chance (Bad Scientist, 2025).
The Framework
CausalForge is a framework for automated theoretical research in causal inference grounded in the Lean proof assistant. It combines:
- Causalean — a foundational Lean library for causal inference containing 7,035 machine-checked declarations, developed with language-model assistance under human design and review.
- CausalSmith — a self-improving agentic pipeline that selects research topics, proposes results, formalizes statements, constructs proofs, and presents the resulting outcomes for human inspection.
- Paper: arXiv:2607.22511
- Source code, formal library, and run logs: https://github.com/Jiyuan-Tan/CausalForge
Key Insight: Statement Audits
Machine-checked proofs only establish the logical validity of a formalized statement from its assumptions—not whether that statement faithfully captures the intended scientific claim. To address this gap, the pipeline supplements kernel-level verification with statement audits, comparing each formalized theorem against the informal claim it is meant to express.
Evaluation
The system is evaluated using the outputs produced by a completed autonomous research run.