CausalForge combines Lean proofs with automated causal research
Automated theory research keeps hitting the same wall: models can draft papers faster than anyone can tell if the theorems are real. arXiv 2607.22511 answers with CausalForge — a Lean-grounded loop from Jiyuan Tan and Vasilis Syrgkanis that tries to make causal-theory agents accountable to a proof kernel, not another LLM reviewer.
The authors’ dig at the status quo is blunt. Prior work shows LLM “review boards” can accept fabricated papers at high rates and catch fakes near chance. CausalForge’s bet is different: machine-checked Lean 4 proofs, plus an audit that the formal statement still means the claim in English.
What Causalean puts in Lean 4
The substrate is Causalean, a Lean 4 library of causal inference built with language-model drafting under human design and review. The compiled index holds 7,035 machine-checked declarations across 973 files — about 4,616 theorems, 2,015 definitions, and hundreds of structures and instances — spanning graphs and SCMs, potential outcomes, identification, panel methods, experimentation, estimation, and asymptotic statistics.
That breadth is the point. Agents should not rebuild backdoor adjustment or DML asymptotics from scratch each run. The library is sorry-free by the authors’ audit, with retrieval over concept, type pattern, and open proof goals so the pipeline can compose verified primitives instead of inventing vacuous shells.
How CausalSmith proposes and proves claims
CausalSmith is the agentic pipeline on top: Discovery, Formalization, Proof Construction, and Presentation. It can accept a researcher topic or pick one, propose a result in natural language, map it onto a logic graph of statements, scaffold Lean declarations, fill proofs against the live compiler, and assemble a paper linked back to the formal objects.
Runs are recorded either way. Across 132 banked runs, 11 were accepted as sound, novel at the requested tier, and fully proved; 51 were downgraded as sound but not novel enough; 70 failed. Accepted work clusters in estimation, experimentation, and panel methods. Pure identification and SCM questions mostly stall — often because the “new” claim collapses into a known construction once the math is written out.
Why statement-faithfulness audits sit atop the kernel
A Lean kernel acceptance only proves the term has the claimed type. It does not prove the theorem is the scientific claim you thought you made. The paper catalogs the failure modes that still type-check: wrong statements, definitions that unfold to True, axioms standing in for proofs, dropped hypotheses, hardcoded constants.
CausalForge’s answer is a statement-faithfulness audit over the logic graph. Nodes carry natural-language intent and Lean text; reviewers mark match or drift; mechanical scans reject sorry, admit, and sneaky axioms; a final dual-model convergence pass rechecks the frozen graph. Kernel soundness and statement match are separated on purpose. Importance stays a human call.
The ATE minimax gap result and limits
The flagship accepted result closes a published minimax gap for average treatment effect estimation under high-dimensional discrete confounding. Prior work left a log² gap between upper and lower bounds. CausalSmith’s run produces a hybrid heavy/light-cell estimator that attains the sharp rate, formalized across twenty-six Lean modules, with the imported lower bound carried as a cited hypothesis rather than a hidden axiom.
Code, library, and run records sit at the authors’ GitHub; a companion site browses declarations and accepted write-ups. Limits are explicit: the audit itself still uses LLMs, novelty tiers are LLM judgments, the accepted catalogue is small, and conceptual identification breakthroughs are rare compared with technical gap-closing.
Analysis: CausalForge does not solve automated science. It draws a cleaner line between a compiling proof, a faithful statement, and a result anyone should care about — and that line is the part most agent-scientist demos keep blurring.
