The exact contents of citations.db main_text.text for this paper — one flattened LaTeX string, title through conclusion, appendix excluded, unmodified except for removing email addresses. This is what our citation measures are computed over.
73,424 characters
CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
\maketitle
\begin{abstract}
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~\citep{badscientist2025}. We present \textsc{CausalForge}, a framework for automated theoretical research in causal inference grounded in the Lean proof assistant. \textsc{CausalForge} combines \textsc{Causalean}, a foundational Lean library for causal inference containing 7,035 machine-checked declarations developed with language-model assistance under human design and review, with \textsc{CausalSmith}, a self-improving agentic pipeline that selects research topics, proposes results, formalizes statements, constructs proofs, and presents the resulting artifacts for human inspection. Because a machine-checked proof establishes only that a formal statement follows from its assumptions—not that the statement faithfully captures the intended scientific claim—the pipeline augments kernel verification with a statement audit that compares each formal theorem against the informal claim it is intended to express. We evaluate the system using artifacts produced by completed autonomous research runs. The source code, formal library, and run records are available at \url{https://github.com/Jiyuan-Tan/CausalForge}.
\end{abstract}
\section{Introduction}
\label{sec:intro}
Language models can now generate research artifacts---conjectures, proofs,
experiments, and complete papers---more rapidly than they can be evaluated. In
empirical fields, this primarily increases the burden of review. In theoretical work,
it presents a more direct risk: an incorrect theorem may be indistinguishable from a
correct one until it is verified by an expert, but expert verification is
slow and costly. Many systems for automated mathematical and theoretical research
address this bottleneck by delegating evaluation to another language model: one model proposes
and another reviews, with the review model supplying the main evaluation signal.
Empirical evaluations already show the defects of LLM reviewers. Independent evaluations of the
AI-Scientist systems~\citep{aiscientist2025} report hallucinated numbers, frequent
coding failures, and little genuine novelty~\citep{aiscientist_eval2025}. More
concerningly, \citet{badscientist2025} show that a calibrated board of LLM reviewers
accepts deliberately fabricated papers up to $82\%$ of the time while detecting the
fabrication at near-chance rates. These findings make LLM review an unreliable evaluator of correctness.
Formal verification provides a different basis for evaluation. When a theorem is
formalized in \textsf{Lean~4}{} and its proof is accepted by the kernel, the proof is guaranteed
to be correct relative to \textsf{Lean~4}{}'s trusted core. This guarantee is unavailable to an LLM reviewer and
removes proof soundness from the model's judgment. However, simply asking an LLM to verify its claims in \textsf{Lean~4}{} runs into two obstacles: cost and faithfulness.
The first obstacle is cost. Formalizing a result from first principles is slow and labor-intensive.
Causal inference needs a reusable library of identification theorems, estimators, and
asymptotic results. Such a library lets each proof begin from verified causal
infrastructure, which spares every run the work of rebuilding standard theory from
scratch. The second obstacle is the match between the formal theorem and the
intended claim. Passing the type checker establishes proof validity while leaving this
match to be checked. A statement can be
free of \texttt{sorry} and still be mathematically uninformative: a definition may reduce to
\texttt{True}; or an unproven step may be introduced as an \texttt{axiom} that the kernel
accepts. Recent work documents this gap from several angles~\citep{sorries2026,
signalcoverage2026,beyondkernel2026}, and we observed it in our own runs as well. In one, an
agent converted difficult lemmas into \texttt{axiom}s, yielding a type-checking shell
with axioms substituting for proof. In another, the model altered a hypothesis, so the
\textsf{Lean~4}{} code proved a statement different from the one the paper claimed. Both cases are kernel-acceptable;
detecting these failures requires assessing the statement as well as the proof. The
central question is therefore whether the formal statement expresses the intended
claim. Our pipeline answers it with a fine-grained audit step
(\Cref{sec:pipeline-audit}) that compares each formal statement with the claim it is
meant to express, so that the \textsf{Lean~4}{} development faithfully represents the
natural-language result. Together with the kernel, this audit supports a two-part
guarantee: the proofs the pipeline produces are machine-checked, and the statements
they establish are the ones the paper reports.
We instantiate this approach in causal inference through \textsc{CausalForge}{}, which has
two components. \textsc{Causalean}{} is a \textsf{Lean~4}{} library covering the causal-inference
toolkit, giving agents verified primitives to compose. It was itself built with
language-model assistance: humans chose what to formalize and how to state it, agents
drafted the definitions, proofs, and docstrings under those decisions, and a human
then reviewed the resulting \textsf{Lean~4}{} statements. \textsc{CausalSmith}{} is
a self-improving agentic pipeline that selects or accepts a research topic, proposes a result,
formalizes it, proves it, and presents it. The pipeline represents each result as a logic graph whose nodes are
statements, checks each node against the intended claim, and promotes missing lemmas into
\textsc{Causalean}{} once they have been proved and reviewed. The system distinguishes two
layers of trust: the kernel establishes proof soundness; the statement audit
checks whether the formal statement matches the intended claim.
\paragraph{Contributions.}
\begin{itemize}[leftmargin=1.4em,itemsep=1pt,topsep=2pt]
\item \textsc{Causalean}{}, a broad \textsf{Lean~4}{} formalization of causal inference spanning
graphical and structural causal models, potential outcomes and identification,
panel methods, experimentation, estimation, and statistical theory. It comprises
$7{,}035$ machine-checked declarations, was written with language-model assistance
under human design, and provides a retrieval interface for
agents (\Cref{sec:library}).
\item \textsc{CausalSmith}{}, an end-to-end pipeline whose Discovery stage can select its
own research topic and propose a causal-inference result, which the pipeline then
formalizes, proves, and presents. It also contains a library feedback loop that
grows \textsc{Causalean}{} with the reusable lemmas and theorems its runs demand
(\Cref{sec:pipeline,sec:pipeline-audit}).
\item An evaluation drawn from $123$ recorded runs: a catalogue of machine-checked
results and a headline result found by the system, which closes a gap in \citet{zeng2024discrete}
(\Cref{sec:eval}). The catalogue also exposes an asymmetry in what the system
proposes well: when it chooses its own question, its accepted results are
concentrated in questions where the literature has already located the gap and the
missing work is technical, while questions whose contribution would have to be a new
idea are downgraded for reducing to known constructions
(\Cref{sec:eval-question-type}).
\end{itemize}
\paragraph{Availability.}
The \textsc{Causalean}{} library, the \textsc{CausalSmith}{} pipeline, and the run record backing
\Cref{sec:eval} are available at \url{https://github.com/Jiyuan-Tan/CausalForge}. A
companion site at \url{https://jiyuan-tan.github.io/CausalForge/} provides a browsable
view of the library, including the natural-language statement of each declaration and
the generated write-up of each accepted result.
\Cref{tab:positioning} places \textsc{CausalForge}{} against the systems it invites
comparison with. Automated theorem provers prove statements they are handed;
automated-research agents propose statements and leave theorem verification outside
their core workflow; benchmarks test causal competence against fixed labeled
answers. \textsc{CausalForge}{} contributes the combination of proposing a causal theorem and
auditing that its formal statement means what was claimed.
\begin{table}[t]
\centering
\footnotesize
\setlength{\tabcolsep}{4.5pt}
\caption{Where \textsc{CausalForge}{} sits among neighboring systems. ``Statement
audit?'' asks whether a system checks that the formal statement means the intended
claim, beyond type-checking.}
\label{tab:positioning}
\begin{tabular}{lccccc}
\toprule
System & Proposes & Machine-checked & Statement & Evaluator & Self- \\
& theorem? & proof? & audit? & soundness & improving? \\
\midrule
AI Scientist~\citep{aiscientist2025} & \checkmark & --- & --- & LLM judge & --- \\
FunSearch\,/\,AlphaEvolve~\citep{funsearch2024,alphaevolve2025} & partial & \checkmark & --- & task metric & \checkmark \\
AlphaProof~\citep{alphaproof2025} & --- & \checkmark & n/a & sound & partial \\
Causal benchmarks~\citep{cladder2023,corr2cause2024} & --- & --- & --- & fixed labels & --- \\
Causal agents~\citep{causalcopilot2024} & --- & --- & --- & none & --- \\
\textbf{\textsc{CausalForge}{} (ours)} & \checkmark & \checkmark & \checkmark & sound + audit & \checkmark \\
\bottomrule
\end{tabular}
\end{table}
\section{Related Work}
\label{sec:related}
\paragraph{Autoformalization, theorem proving, and statement matching.}
A large body of work uses language models with proof assistants, from neural proof
search~\citep{gptf2020,htps2022} and early autoformalization~\citep{wu2022autoform,dsp2022}
to whole-proof generation and repair~\citep{baldur2023},
retrieval-augmented provers~\citep{leandojo2023,deepseekprover2025}, and
competition-level systems~\citep{alphageometry2024,alphaproof2025}. These systems are
usually measured on benchmarks of known problems, including MiniF2F,
ProofNet, and PutnamBench~\citep{minif2f2021,proofnet2023,putnambench2024}. Our
setting lacks the fixed reference on which these methods rely: because the theorems
are new, there is no gold statement or proof against which to evaluate them. This
precludes reference-equivalence scoring and requires an explicit assessment of
whether the formal statement matches the intended claim. Recent studies demonstrate that passing the kernel is not equivalent to
stating the intended
theorem---\texttt{sorry}-free formalizations still fail expert
review~\citep{sorries2026}, type-correct statements can be semantically
wrong~\citep{signalcoverage2026,beyondkernel2026}, and vacuity and reward hacking are
common enough to benchmark~\citep{formalreward2026}. Proposed remedies include
roundtrip and back-translation equivalence
checks~\citep{faithfulnessgap2026,roundtrip2026,backtrans2024}, learned alignment
scorers between a statement and its formalization~\citep{formalalign2025}, and a
rejection of surface-overlap metrics as evidence of a correct statement
match~\citep{bleu_disavow2024}. We operationalize these findings as an audit within
a discovery loop, localized over a proof-dependency graph in the style of Lean
blueprints and proof-flow tools~\citep{leanarchitect2026,proofflow2025}. The broader
shift toward proof-assistant-grounded reasoning~\citep{formalfrontier2024} provides the
context in which this system operates for causal inference.
\paragraph{Automated research agents and verified discovery.}
Agentic systems that carry out end-to-end research~\citep{aiscientist2025} are
vulnerable when an LLM judges their output, whether by independent
re-evaluation~\citep{aiscientist_eval2025} or by adversarial
construction~\citep{badscientist2025}. A complementary tradition grounds discovery in
a hard verifier---program search against a fitness
function~\citep{funsearch2024,alphaevolve2025} or a proof against a kernel. Between
these poles sit hypothesis-generating ``co-scientist'' agents that propose and refine
scientific claims but validate them empirically rather than
formally~\citep{aicoscientist2025}. We use a hard verifier for proof soundness and add
an audit of whether the specification is the intended one, a task that their fixed
specifications do not require.
\paragraph{LLMs for causal inference.}
A parallel literature examines whether language models can reason causally. It divides
into three strands, each treating causal reasoning as something to test or deploy
rather than something to prove; recent surveys organize this work by causal task
and intervention level~\citep{ma2025causal}. Benchmarks measure whether models answer
causal queries or choose valid research designs---CLadder and Corr2Cause on graphical
and correlational reasoning~\citep{cladder2023,corr2cause2024}, CaLM and QRData on
broad and data-grounded causal question answering~\citep{calm2024,qrdata2024}, and,
closest to our own domain, benchmarks that target end-to-end causal inference on real
scientific studies and disentangle identification from
estimation~\citep{causcibench2025,causalbench_ours2026}. Across these benchmarks,
surface accuracy can conceal shallow, retrieval-driven reasoning. A critical strand
finds that models can explain causal language while hallucinating the
reasoning~\citep{gao2023chatgptcausal}, recite memorized causal facts rather than
reason interventionally~\citep{causalparrots2023}, commit elementary causal
fallacies~\citep{fallacies2024}, and are flattered by benchmarks solvable through
knowledge lookup~\citep{causalreview2024}. A third strand builds agents that
do causal analysis, automating discovery, data preparation, and estimator
selection but offering no correctness guarantee~\citep{kiciman2023causal,matmcd2024,
orca2025,causalcopilot2024}. Closest to us in form are agentic systems for causal
inference itself: end-to-end pipelines that map a dataset and question to a chosen
estimator and result~\citep{causalaiscientist2026}, LLM-assisted search for
instrumental variables~\citep{miningcausality2024}, and the multi-agent IV
Co-Scientist~\citep{ivcoscientist2026}, which proposes, critiques, and refines
candidate instruments. These share our propose-and-critique structure but validate
their output statistically or empirically; none produces a machine-checked causal
theorem.
Work pairing language models with formally verified causal inference appears to
be limited to theorem-proving systems that verify general mathematics rather than
causal inference~\citep{leancopilot2024} and to the causal-LLM line above, which does
not provide formal verification. \textsc{CausalForge}{} addresses this intersection.
\paragraph{The closest related systems.}
Two efforts are particularly closely related. A Lean library for economics~\citep{econcslib2026}
formalizes established economic theory, and a multi-agent system formalizes asymptotic
statistical theory with auditor and reviewer agents that already guard against
vacuity~\citep{asymptoticstats2026}. \textsc{CausalForge}{} differs in three respects: it discovers novel results rather
than formalizing known ones; it audits statement--claim matches node by node over an
explicit logic graph, so a change re-opens only the affected nodes; and it grows its
reusable library by promoting proved lemmas for later runs.
Although anti-vacuity auditing is established prior art,
graph-localized, incremental auditing within a self-improving discovery loop is the
contribution advanced here.
\section{Background}
\label{sec:prelim}
\paragraph{Causal inference.}
Causal inference concerns the consequences of intervention rather than observation
alone. Two frameworks are widely used in the field: structural causal models (SCMs)
and potential outcomes (PO). An SCM models causal relationships with a directed acyclic graph and represents
interventions with the $\mathrm{do}$-operator; its classical results include the graphical
identification criteria delivered by do-calculus and the ID algorithm. Potential outcomes instead attach to each unit a family of
counterfactual responses, one per treatment level, and write causal estimands---the
average treatment effect, the effect on the treated, difference-in-differences, the
local average treatment effect---as functionals of their joint distribution. An
estimand is identified when it is a function of the observational distribution
alone and only partially identified when the data pin it to a set rather than
a point, as with Manski or Balke--Pearl bounds. \textsc{Causalean}{} (\Cref{sec:library})
formalizes most classical results under these frameworks.
\paragraph{\textsf{Lean~4}{} as a proof checker.}
\textsf{Lean~4}{} is an interactive theorem prover and programming language in which
mathematics is written in a fully formal language~\citep{lean42021}. A definition is
a term, a proposition is a type, and a proof of that proposition is a term of that
type, so checking a proof reduces to type-checking a term. A user does not write such
terms directly: they write \emph{tactics}---commands such as \texttt{intro},
\texttt{simp}, or \texttt{induction} that manipulate an explicit goal state---and the
system elaborates them into a proof term. Mathlib, \textsf{Lean~4}{}'s community mathematics
library, supplies the analysis, probability, and measure theory that a
causal-inference development builds on~\citep{mathlib2020}.
What makes this useful as an evaluator is where the trust sits. The elaborator, the
tactic language, and any model that wrote the tactics are all untrusted; only a small
kernel decides whether the final term has the claimed type. When the kernel accepts a
term of type $\tau$, $\tau$ is provable in \textsf{Lean~4}{}'s underlying type theory, and the
kernel also reports which axioms the proof depends on. We call this property proof
soundness. It is a guarantee about the proof and not about the statement: whether
$\tau$ is the proposition the researcher intended to prove is a separate question,
which \Cref{sec:pipeline-audit} takes up.
\section{The \textsc{Causalean}{} Library}
\label{sec:library}
The cost of formalizing results from first principles limits automated discovery, and
\textsc{Causalean}{} supplies the reusable foundation that discovery needs. It is a foundational \textsf{Lean~4}{} library of
causal inference that gives agents verified results to compose across runs. For
example, a proof that requires the backdoor adjustment formula or
the asymptotic normality of a debiased estimator can reuse a result that has already
been stated and proved. This section describes the library's contents and the design
properties---breadth, stability, and searchability---required by a research pipeline.
\subsection{Design and scope}
\label{sec:library-design}
\label{sec:library-scale}
\textsc{Causalean}{} holds paper-agnostic mathematics: the definitions and theorems any
causal result might reuse. One-off lemmas of a particular paper live instead in the
pipeline package, and continuous integration enforces the separation: runs read from
the core freely but write back to it only through the explicit human promotion step
in \Cref{sec:pipeline-study}.
The library was built with LLM assistance rather than written by hand, and
the division of labor follows the trust model of \Cref{sec:intro}. Humans set the
scope, choose which results to formalize, and fix the definitions that later theorems
are stated against; agents then draft the statements, proofs, and docstrings,
iterating against the compiler; and a human reads the resulting \textsf{Lean~4}{} statements
before they are kept. Nothing enters the library until the kernel accepts it and it
survives the same unproved-shortcut screen the pipeline applies to its own output
(\Cref{sec:library-axiom-checks}). The human then checks that the formal statement
matches the intended claim and that it is stated in a standard form.
Two smaller conventions keep the library usable by an agent: each declaration's prose
lives once in its \textsf{Lean~4}{} docstring, from which the human-readable API is
regenerated, so documentation stays aligned with code; and files stay small and hold a
single topic, so a retrieved declaration arrives with enough surrounding context to
apply it.
The compiled environment index records $7{,}035$ declarations: $4{,}616$ theorems,
$2{,}015$ definitions, and $404$ structures, instances, and inductive types,
across $973$ files and roughly $262{,}000$ lines (\Cref{tab:coverage}).\footnote{These
repository statistics are a snapshot. The totals may increase because the
\textsc{CausalSmith}{} pipeline runs continuously and can promote newly proved, reusable
declarations to \textsc{Causalean}{}.} Ten
clusters cover the field from graphical foundations to asymptotic statistics.
\begin{table}[t]
\centering
\small
\caption{\textsc{Causalean}{} coverage by cluster. All figures are read from the compiled
environment index (\texttt{lake exe library\_index}); the per-cluster kind columns
sum to the grand total. ``s/c/i'' abbreviates the remaining declaration
kinds---structures and classes, inductives, and instances.}
\label{tab:coverage}
\begin{tabular}{lrrrrr}
\toprule
Cluster & Files & Lines & Defs & Thms/Lem. & s/c/i \\
\midrule
Estimation & 168 & 54{,}246 & 298 & 621 & 100 \\
Stat & 202 & 47{,}165 & 213 & 894 & 38 \\
PO & 138 & 41{,}415 & 592 & 947 & 80 \\
SCM & 88 & 36{,}342 & 208 & 523 & 67 \\
Mathlib (local) & 113 & 24{,}778 & 104 & 500 & 11 \\
Panel & 68 & 18{,}382 & 258 & 389 & 44 \\
Experimentation & 101 & 16{,}095 & 172 & 370 & 12 \\
Graph & 21 & 10{,}866 & 70 & 160 & 28 \\
ML & 50 & 6{,}330 & 56 & 100 & 13 \\
Discovery & 24 & 6{,}321 & 44 & 112 & 11 \\
\midrule
\textbf{Total} & \textbf{973} & \textbf{261{,}940} & \multicolumn{3}{c}{\textbf{$7{,}035$ declarations}} \\
\bottomrule
\end{tabular}
\end{table}
\begin{figure}[t]
\centering
\begin{tikzpicture}[
font=\footnotesize, node distance=3mm,
lay/.style={rounded corners=3pt, draw, line width=0.7pt, minimum height=10mm,
align=center, text width=66mm, text=cInk},
found/.style={lay, fill=cGrayBg, draw=cGray},
core/.style={lay, fill=cBlueBg, draw=cBlue},
app/.style={lay, fill=cGreenBg, draw=cGreen},
idx/.style={rounded corners=3pt, draw=cAmber, line width=0.8pt, fill=cAmberBg,
minimum height=43mm, text width=22mm, align=center, text=cInk},
up/.style={-{Stealth[length=4pt]}, line width=0.7pt, draw=cGray},
]
\node[found] (found) {\textbf{Foundations}\\[1pt]{\scriptsize Graph (DAG, $d$-sep, SWIG) $\cdot$ local Mathlib}};
\node[core, above=of found] (core) {\textbf{Models}\\[1pt]{\scriptsize SCM \& do-calculus $\cdot$ potential outcomes $\cdot$ asymptotic statistics}};
\node[app, above=of core] (idpar) {\textbf{Identification}\\[1pt]{\scriptsize exact (ATE/DiD/LATE) $\cdot$ partial (Manski, Balke--Pearl)}};
\node[app, above=of idpar] (est) {\textbf{Methods}\\[1pt]{\scriptsize estimation (DML, minimax) $\cdot$ panel $\cdot$ experimentation $\cdot$ discovery}};
\node[idx, anchor=west] at ($(est.east)!0.5!(found.east) + (8mm,0)$) (idx)
{\textbf{Retrieval}\\[4pt]{\scriptsize $7{,}035$ decls}\\[3pt]{\scriptsize concept $\cdot$ type}\\[1pt]{\scriptsize goal $\cdot$ semantic}};
\begin{scope}[on background layer]
\draw[up] (found.north) -- (core.south);
\draw[up] (core.north) -- (idpar.south);
\draw[up] (idpar.north) -- (est.south);
\end{scope}
\draw[{Stealth[length=4pt]}-{Stealth[length=4pt]}, dashed, line width=0.7pt, draw=cAmber]
($(est.east)!0.5!(found.east)$) -- (idx.west);
\end{tikzpicture}
\caption{\textsc{Causalean}{} in layers: graphical and measure-theoretic foundations support
the model languages, which support identification, which supports the estimation and
design methods on top. A retrieval index over all $7{,}035$ declarations spans the
stack and is the interface the pipeline queries.}
\label{fig:causalean}
\end{figure}
\subsection{A tour of the clusters}
\label{sec:library-tour}
The library layers from graphical and measure-theoretic foundations up to the
estimation and design methods that depend on them (\Cref{fig:causalean}).
\paragraph{Graphs and structural models.}
The Graph cluster builds directed acyclic graphs with a decidable edge
relation and a stored topological order, on top of which sit the parent, child, and
ancestor operations, $d$-separation implemented as Bayes-Ball reachability,
single-world intervention graphs, and the $c$-component decomposition that the
identification algorithm needs. The SCM cluster turns these graphs into
structural causal models. It defines interventions and the $\mathrm{do}$-operator,
proves the semi-graphoid axioms that justify do-calculus, represents factored
kernels, and develops graphical identification proper: backdoor and frontdoor
adjustment, general adjustment criteria, and a soundness proof for the ID algorithm
on the discrete positive class. This is the part of the library where a causal query
becomes a formula in the observational distribution, or receives an explicit
nonidentification certificate.
\paragraph{Potential outcomes and identification.}
The PO cluster is the largest by definitional surface, because it carries the
two identification branches the pipeline uses most. Exact identification covers the
standard estimands---ATE, ATT, difference-in-differences and its Callaway--Sant'Anna
group-time refinement, LATE, regression discontinuity, proximal and dynamic-treatment
designs---each stated as an equality between a counterfactual contrast and an
estimable functional. Partial identification covers the bounds one falls back on when
point identification is impossible: Manski's worst-case bounds with their
monotone-treatment-response and instrument refinements, the sharp Balke--Pearl bounds
for a binary instrument, Lee's trimming bounds under selection, marginal-sensitivity
models, and Imbens--Manski inference for the resulting sets.
\paragraph{Estimation and asymptotic statistics.}
Estimation, the largest cluster by volume, is the semiparametric machinery:
double/debiased machine learning for the ATE, ATT, and CATE; efficient influence
functions obtained by projection onto a tangent space; structure-agnostic minimax
lower bounds with matching estimators; and convergence rates for nonparametric
instrumental variables. These results draw on the
Stat cluster, which formalizes the probability and empirical-process theory
underneath: central limit theorems, U-statistics with their H\'ajek projections,
Glivenko--Cantelli and bracketing-entropy tools, M- and Z-estimation, concentration
inequalities, and the bootstrap. Because these results live in the library, an
estimation proof can cite a limit theorem directly and focus on the causal argument.
\paragraph{Panel, experiments, and discovery.}
The remaining clusters round out the toolkit. Panel characterizes the
estimands that two-way fixed-effects and difference-in-differences regressions
actually recover, including the negative-weights decomposition and event-study
contamination that motivate modern DiD estimators. Experimentation develops
experimentation theory, including randomization inference, Horvitz--Thompson
estimation, Neyman allocation, and central limit theorems under network interference.
Discovery formalizes identifiability results for causal structure learning,
such as LiNGAM under non-Gaussianity and invariant prediction, while ML and
the local Mathlib supplements provide the learning-theory and measure-theoretic
lemmas the rest of the library draws on.
\subsection{Flagship results}
\label{sec:library-flagship}
The library also provides a collection of classical flagship results from the literature. \Cref{tab:flagship}
catalogues the principal substantive result families across the library's major
research areas. Each entry is a named declaration with a machine-checked proof;
\Cref{app:flagship} gives its source location. Curators have also marked $1{,}597$
library theorems as headline results and recorded $3{,}677$ statement-level review
stamps, each a human assessment of whether the formal statement matches the intended
claim.
\begin{longtable}{@{}>{\raggedright\arraybackslash}p{0.52\textwidth} >{\raggedright\arraybackslash\ttfamily\scriptsize}p{0.40\textwidth}@{}}
\caption{Flagship theorems across \textsc{Causalean}{}'s major research areas. Each entry
is a named, machine-checked declaration; long identifiers may wrap.}
\label{tab:flagship} \\
\toprule
\normalfont Result & \normalfont\rmfamily\small Declaration \\
\midrule
\endfirsthead
\multicolumn{2}{@{}l}{\small\itshape Table \thetable\ continued} \\
\toprule
\normalfont Result & \normalfont\rmfamily\small Declaration \\
\midrule
\endhead
\bottomrule
\endfoot
\multicolumn{2}{@{}l}{\textit{Graphical and structural causal models}} \\
Markov equivalence iff two DAGs have the same skeleton and immoralities & markovEquiv\_\allowbreak iff\_\allowbreak sameSkeleton\_\allowbreak sameImmoralities \\
Rule 2 of do-calculus under its graphical condition & do\_\allowbreak rule2\_\allowbreak kernel \\
Backdoor adjustment identifies an interventional distribution almost everywhere & backdoor\_\allowbreak identifiable\_\allowbreak ae \\
Frontdoor adjustment identifies an interventional distribution almost everywhere & frontdoor\_\allowbreak identifiable\_\allowbreak ae \\
Soundness of the graphical ID algorithm on the discrete positive class & id\_\allowbreak sound\_\allowbreak discrete \\
\addlinespace
\multicolumn{2}{@{}l}{\textit{Causal discovery}} \\
LiNGAM identifiability from nonzero source kurtosis & lingam\_\allowbreak identifiability\_\allowbreak kurtosis \\
Soundness of invariant causal prediction & icp\_\allowbreak sound \\
Completeness of invariant prediction for linear-Gaussian models & icp\_\allowbreak complete\_\allowbreak linearGaussian \\
Identifiability in linear causal disentanglement & disentanglement\_\allowbreak identifiability \\
\addlinespace
\multicolumn{2}{@{}l}{\textit{Potential outcomes, exact identification, and partial identification}} \\
Wald-ratio identification of the local average treatment effect & late\_\allowbreak wald \\
Difference-in-differences identification of the ATT & att\_\allowbreak did \\
Callaway--Sant'Anna group-time ATT identification & att\_\allowbreak csdid \\
Sharp regression-discontinuity identification & rdd\_\allowbreak identification \\
Fuzzy regression-discontinuity identification & frd\_\allowbreak identification \\
Wald identification for dynamic treatment timing & whenToTreat\_\allowbreak wald \\
Manski worst-case ATE bounds & manski\_\allowbreak bounds\_\allowbreak ATE \\
Sharpness of the Balke--Pearl bounds for a binary instrument & balkePearl\_\allowbreak sharp \\
Lee bounds for the ATT under selection & lee\_\allowbreak bounds\_\allowbreak ATT\_\allowbreak AS \\
Pointwise Imbens--Manski coverage for partially identified parameters & imbensManski\_\allowbreak pointwise\_\allowbreak coverage \\
\addlinespace
\multicolumn{2}{@{}l}{\textit{Estimation and statistical theory}} \\
Asymptotic normality of the debiased-ML ATE estimator & dml\_\allowbreak ATE\_\allowbreak tendstoNormal \\
Attainment of the Hahn efficiency bound by debiased-ML ATE & dml\_\allowbreak ATE\_\allowbreak attains\_\allowbreak hahn\_\allowbreak bound \\
Asymptotic linearity of debiased-ML ATT estimation & dml\_\allowbreak ATT\_\allowbreak isAsymLinear \\
Asymptotic normality of partially linear DML & plr\_\allowbreak dml\_\allowbreak tendstoNormal \\
Asymptotic linearity of sequential doubly robust DTR estimation & seqDR\_\allowbreak dml\_\allowbreak isAsymLinear \\
Structure-agnostic minimax lower bound for ATE estimation & minimax\_\allowbreak lower\_\allowbreak bound\_\allowbreak var\_\allowbreak causal \\
Optimal weighting for generalized method of moments & gmm\_\allowbreak efficiency \\
Central limit theorem for regular order-$m$ U-statistics & uStatisticOrder\_\allowbreak clt \\
\addlinespace
\multicolumn{2}{@{}l}{\textit{Panel and event-study methods}} \\
Causal decomposition of staggered-adoption TWFE into weighted contrasts & twfe\_\allowbreak po\_\allowbreak decomposition \\
Characterization of linear-unbiased BJS imputation estimators & bjs\_\allowbreak linear\_\allowbreak unbiased\_\allowbreak iff\_\allowbreak imputation\_\allowbreak form \\
Event-study pretrends induced by post-treatment effects & apparent\_\allowbreak pretrends\_\allowbreak from\_\allowbreak post\_\allowbreak treatment\_\allowbreak of\_\allowbreak cellGrid \\
\addlinespace
\multicolumn{2}{@{}l}{\textit{Experimentation under interference}} \\
Consistency of Horvitz--Thompson estimation under unknown interference & htEst\_\allowbreak consistent\_\allowbreak eate \\
Central limit theorem for a two-stage interference direct effect & directEffect\_\allowbreak clt \\
Stein-method CLT for estimators under network interference & localDependenceCLT\_\allowbreak of\_\allowbreak stein \\
Wald coverage under network interference & wald\_\allowbreak coverage\_\allowbreak of\_\allowbreak stein \\
\end{longtable}
\subsection{Retrieval}
\label{sec:library-retrieval}
A library of this size requires effective declaration retrieval, so retrieval is a
primary component of \textsc{Causalean}{}. During the build, every declaration is elaborated
into an index that records its name, kind, module, source text, docstring,
cross-references, axiom dependencies, and whether its proof uses \texttt{sorry}. A
companion tier embeds all $7{,}035$ declarations with a $1{,}024$-dimensional sentence
encoder. The search engine provides three modes over this index: a concept mode that
expands a natural-language query with causal-inference synonyms, a type-pattern mode
for structural queries, and a goal-directed mode that ranks candidates against an open
proof goal. Each mode can fuse its lexical ranking with the embedding tier and
supports cluster and module filters. This interface lets the pipeline reuse
verified results as composable proof ingredients.
\subsection{Axiom checks and positioning}
\label{sec:library-axiom-checks}
The library passes the axiom checks required for its use as a verified foundation.
All $7{,}035$ declarations are \texttt{sorry}-free, and the corpus is free of
hand-written \texttt{axiom}; the only non-standard axioms are compiler artifacts
introduced by \texttt{native\_decide}, which occur in finite-graph decidability
arguments and several minimax calculations and are reported explicitly. Two
results are not original to \textsc{Causalean}{} but adapted, re-licensed copies of
external \textsf{Lean~4}{} developments, bumped to \textsc{Causalean}{}'s \textsf{Lean~4}{}/Mathlib pin: the
Karush--Kuhn--Tucker first-order necessary conditions under LICQ and affine
constraint qualifications, from OptSuite's \texttt{optlib}~\citep{optlib2025} and
consumed by the Estimation cluster's minimax lower bounds; and Rademacher
complexity, McDiarmid's inequality, symmetrization, and the Dudley entropy
integral, from \texttt{lean-rademacher}~\citep{leanrademacher2025} and consumed
across Stat, Estimation, and ML. Two recent
libraries provide relevant points of comparison---a
Lean formalization of economics and a multi-agent formalization of asymptotic
statistics (\Cref{sec:related}). \textsc{Causalean}{} differs by covering the causal-inference
toolkit and by serving as a library that the research pipeline can compose and
extend, as described in the next section.
\section{The \textsc{CausalSmith}{} Pipeline}
\label{sec:pipeline}
\textsc{CausalSmith}{} operationalizes the library within a research pipeline. There are four stages in our pipeline: Discovery, Formalization, Proof Construction, and Presentation. The pipeline
either accepts a researcher-supplied topic or selects one before proposing a
causal-inference result in natural language. The pipeline then formalizes the result, proves it in
\textsf{Lean~4}{}, and produces a paper linked to the formal development. Once the Discovery stage fixes
the intended claim, the central object throughout the pipeline is a logic
graph. Discovery creates this graph; formalization
maps its nodes to planned \textsf{Lean~4}{} declarations; proof construction fills those
declarations and updates their dependencies; statement matching checks each formal
node against the intended claim; and presentation reads the reviewed graph when it
writes the paper.
Essentially, \textsc{CausalSmith}{} is a deterministic state machine that executes each
stage and retries failures within fixed limits. A lightweight orchestrator launches
the state machine, records its verdicts, and requests human input only at a few
fixed decision points. In the automatic mode used for most runs, the orchestrator
advances through every stage on its own and pauses for a person only at the final
acceptance decision, so a typical run completes without a human in the loop. \Cref{fig:pipeline} summarizes
the workflow; \Cref{app:pipeline-spec,app:pipeline-record,app:pipeline-proof-loop,app:pipeline-paper}
give an operational specification of the stages, artifacts, recovery rules, and presentation workflow.
\begin{figure*}[!htb]
\centering
\begin{tikzpicture}[
font=\footnotesize, node distance=18mm,
stage/.style={rounded corners=3pt, draw=cBlue, line width=0.8pt, fill=cBlueBg,
minimum height=13mm, minimum width=27mm, align=center, text=cInk},
gate/.style={rounded corners=2pt, draw=cAmber, line width=0.7pt, fill=cAmberBg,
minimum height=6mm, inner sep=3pt, align=center, font=\scriptsize,
text=cInk},
lib/.style={rounded corners=3pt, draw=cGreen, line width=0.9pt, fill=cGreenBg,
minimum height=12mm, minimum width=34mm, align=center, text=cInk},
bank/.style={rounded corners=3pt, draw=cAmber, line width=0.9pt, fill=cAmberBg,
minimum height=9mm, align=center, text=cInk, inner sep=4pt},
fl/.style={-{Stealth[length=5pt]}, line width=0.9pt, draw=cGray},
dfl/.style={-{Stealth[length=5pt]}, line width=0.9pt, draw=cGreen, dashed},
afl/.style={-{Stealth[length=5pt]}, line width=0.9pt, draw=cAmber, dashed},
]
\node[stage] (disc) {\textbf{Discover}\\[1pt]{\scriptsize propose $\to$ solve}};
\node[stage, right=of disc] (form) {\textbf{Formalize}\\[1pt]{\scriptsize plan $\to$ scaffold}};
\node[stage, right=of form] (prove) {\textbf{Prove}\\[1pt]{\scriptsize fill $\to$ review}\\[1pt]{\scriptsize\itshape kernel-checked}};
\node[stage, right=of prove] (pres) {\textbf{Present}\\[1pt]{\scriptsize assemble \& present}};
\draw[fl] (disc) -- node[gate, above=1.5mm] {novelty\\[-1pt]+ soundness} (form);
\draw[fl] (form) -- node[gate, above=1.5mm] {statement\\[-1pt]match} (prove);
\draw[fl] (prove) -- node[gate, above=1.5mm] {convergence\\[-1pt]review} (pres);
\node[lib, below=12mm of $(form)!0.5!(prove)$] (lib)
{\textsc{Causalean}{} \;\textit{\scriptsize verified library}};
\draw[dfl] (lib.north west) to[out=120,in=-90]
node[left=1pt, font=\scriptsize, text=cGreen, pos=0.6] {reuse} (form.south);
\draw[dfl] (prove.south) to[out=-90,in=60]
node[right=1pt, font=\scriptsize, text=cGreen, pos=0.42, align=center] {study\\mode} (lib.north east);
\node[bank, minimum width=15.5cm, below=8mm of lib] (bank)
{run record \;\textit{\scriptsize prior proposals \& outcomes}};
\draw[afl] (bank.north -| disc.south) --
node[left=1pt, font=\scriptsize, text=cAmber, pos=0.5] {screen} (disc.south);
\draw[afl] (pres.south) --
node[right=1pt, font=\scriptsize, text=cAmber, pos=0.5] {record}
(bank.north -| pres.south);
\end{tikzpicture}
\caption{The \textsc{CausalSmith}{} pipeline. Discovery includes topic selection: when a
researcher does not supply a topic, a dedicated selector searches and ranks
candidate directions, screens them against the run record, and admits a topic only
after an adversarial quality gate. The resulting claim moves left to right through
discovery, formalization, proof, and presentation, clearing a gate between stages (novelty and mathematical
soundness; statement matching; and a final convergence review).
The kernel establishes proof soundness during the proof stage. The convergence
review is an independent dual-model review of the full frozen graph, including
nodes previously marked as matched; the presentation stage then assembles the
reviewed result into a paper. Two feedback channels grow the system
(\Cref{sec:pipeline-study}). Stages reuse \textsc{Causalean}{} through retrieval, and when a
run needs a new load-bearing lemma, study mode proves it and promotes it back
into \textsc{Causalean}{}. In parallel, every run---accepted, downgraded, or
failed---is recorded in the run record, whose entries are consulted during
screening before the next proposal is drafted. The logic graph is the object
that moves through the diagram: Discovery creates it from the selected or supplied
topic, formalization maps it
to \textsf{Lean~4}{}, proof construction updates it, the statement-match and convergence gates
review it, and presentation writes from it. See
\Cref{app:pipeline-spec,app:pipeline-record,app:pipeline-proof-loop,app:pipeline-paper}
for the operational stage flow (\Cref{fig:stage-flow}), run record and recovery,
graph-controlled proof loop, and presentation pipeline.}
\label{fig:pipeline}
\end{figure*}
\subsection{The Logic Graph as a Persistent Run Record}
\label{sec:pipeline-graph}
Dependency graphs for proofs are established practice; Lean blueprints and proof-flow
tools represent developments as DAGs of statements~\citep{leanarchitect2026,
proofflow2025}. \textsc{CausalSmith}{} uses the graph as both a plan and a review record. It
turns the global question ``is this result proved, and does the formal theorem match
the intended claim?'' into node-specific questions that can be revisited when the
corresponding statements change.
Each result is stored as a graph whose nodes are statements---a setup, a definition,
an assumption, a lemma, or the headline theorem---and whose edges record dependencies.
A node carries its natural-language statement and its \textsf{Lean~4}{} declaration, a
review status in $\{\texttt{unreviewed}, \texttt{matched}, \texttt{derived},
\texttt{drift}\}$ recording the current statement match, and a
class: a \textsf{gated}{} node represents substrate missing from \textsc{Causalean}{} and must be
discharged by a proof before the result can be recorded as complete, while a
\textsf{cited}{} node is a borrowed result with
source evidence that sits off the critical path. Assumptions carry a finer label
still---claim refinement, regularity bookkeeping, or library gap---distinguishing a hypothesis that genuinely
narrows the claim from one that is only technical scaffolding. Edges come in two
kinds, \texttt{statement-uses} and \texttt{proof-uses}, which separate what a claim
means from what its proof consumes; a validator rejects duplicate nodes
and malformed dependencies. A typical completed result has on the order of a hundred
nodes and a few hundred edges (\Cref{fig:graph}).
Within Discovery, the selector supplies the topic anchor but does not yet create the
logic graph. The proposal and solver then write the natural-language nodes and their
dependency edges from that anchor. Formalization attaches the intended
\textsf{Lean~4}{} declarations. Proof construction adds the proof dependencies. Statement
matching changes review statuses such as \texttt{matched} or \texttt{drift}. Presentation
then uses the reviewed graph as the source of truth for the paper-to-code crosswalk.
The critical path consists of \textsf{gated}{} nodes: a result is complete when every
gated node has a proof and is marked \texttt{matched}. When a statement changes, the
pipeline returns that node to \texttt{unreviewed} and rechecks the affected frontier and
its dependents.
\begin{figure}[t]
\centering
\begin{tikzpicture}[
node distance=8mm and 11mm, font=\footnotesize,
nd/.style={rounded corners=3pt, draw, minimum height=7mm, minimum width=15mm,
align=center, line width=0.8pt, text=cInk},
matched/.style={nd, fill=cGreenBg, draw=cGreen},
drift/.style={nd, fill=cRedBg, draw=cRed},
unrev/.style={nd, fill=cGrayBg, draw=cGray},
cited/.style={nd, fill=cBlueBg, draw=cBlue, dashed},
suse/.style={-{Stealth[length=4.5pt]}, draw=cInk!65, line width=0.7pt},
puse/.style={-{Stealth[length=4.5pt]}, draw=cInk!65, line width=0.7pt, dashed},
crit/.style={line width=4pt, draw=cGreen!25, line cap=round},
]
\node[matched] (s) {setup};
\node[matched, right=of s] (d1) {def $D_1$};
\node[cited, right=of d1] (a2) {cited $A_2$};
\node[matched, above=of s] (a1) {gated $A_1$};
\node[drift, above=of d1] (l1) {lemma $L_1$};
\node[unrev, above=of a2] (l2) {lemma $L_2$};
\node[matched, above=of l1, minimum width=20mm] (t) {theorem $T$};
\begin{scope}[on background layer]
\draw[crit] (s) -- (a1);
\draw[crit] (a1) -- (t);
\end{scope}
\draw[suse] (s) -- (a1);
\draw[suse] (d1) -- (l1);
\draw[suse] (d1) -- (a1);
\draw[puse] (a2) -- (l2);
\draw[puse] (a1) -- (t);
\draw[suse] (l1) -- (t);
\draw[puse] (l2) -- (t);
\end{tikzpicture}
\caption{A logic graph (schematic). Nodes are statements; fill encodes review status
(\textcolor{cGreen}{\textbf{matched}}, \textcolor{cRed}{\textbf{drift}},
\textcolor{cGray}{\textbf{unreviewed}}); a dashed blue border marks a \textsf{cited}{}
node, borrowed and off the critical path. Solid edges are \texttt{statement-uses},
dashed edges \texttt{proof-uses}. The green underlay traces the critical path of
\textsf{gated}{} nodes the review must clear before final recording.}
\label{fig:graph}
\end{figure}
\subsection{Discovery, formalization, and proof}
\label{sec:pipeline-thmsmith}
The pipeline supports two entry modes. A researcher may supply a topic anchor, or the
main orchestrator may invoke the \texttt{causalsmith-topics} module as the first part of
Discovery. The selector searches recent work, reads theorem-bearing papers and their
citing or follow-up literature in full, and drafts a small slate of directions the
literature leaves open. It then checks candidates against active and recorded runs,
ranks them by mathematical promise and by whether the result would have a concrete
downstream use, and submits the leading candidate to an independent adversarial topic
gate. The gate requires a precise, non-vacuous research object, a defensible
novelty tier (the pipeline's ordered grade of a result's novelty), and a genuine downstream
use before the selector emits the topic anchor, question identifier, and
specialization used to continue Discovery. If bounded re-selection cannot produce an
accepted candidate, the pipeline stops for operator direction instead of spending a
theorem run on an ungrounded topic.
Once an anchor is fixed, the remaining discovery stages derive the result in natural
language and build the graph. A proposer drafts a question and an informal solution, a
novelty-and-duplication gate compares it with the literature and judges whether it is
novel, and a solver derives a formalizable mathematical core in natural language. These
outputs become the initial graph nodes and edges. When a proposed claim is too
strong, the solver may narrow it to a valid result, but it may not weaken a statement
merely to complete a proof or strengthen a hypothesis merely to obtain a result. A sound but insufficiently
novel proposal is downgraded, whereas an incorrect or trivial proposal is rejected.
Formalization turns this graph into a proof plan. Each node receives an
intended \textsf{Lean~4}{} declaration, a module location, and either a proof obligation or a
reuse target from \textsc{Causalean}{}. The plan is translated into a scaffold with proof
obligations. A review-and-fill loop then resolves these obligations. On each
iteration, the reviewer first checks that every declaration remains aligned with the
graph and repairs only declarations whose statements have changed; it then fills the
remaining obligations, using the retrieval interface in
\Cref{sec:library-retrieval} to reuse existing results. A deterministic lint flags
hypotheses unused by the proof, which may indicate a vacuous or mis-stated theorem.
\subsection{Statement matching}
\label{sec:pipeline-audit}
The statement-match gate in \Cref{fig:pipeline} is the statement faithfulness audit.
The \textsf{Lean~4}{} kernel establishes proof soundness, but, as \Cref{sec:prelim} notes, it does not
establish that the formal statement is the one the researcher meant to prove: the kernel accepts a
theorem whose hypotheses are contradictory, a definition that unfolds to \texttt{True},
or a lemma asserted as an \texttt{axiom} in place of a proof. This gate checks whether
each formal statement still matches the intended claim stored in its graph node. The
target is logical equivalence: the intended claim and the \textsf{Lean~4}{} declaration must have
equivalent assumptions and conclusions, with neither statement stronger nor weaker than
the other. The two do diverge in practice: a development can be free of \texttt{sorry} and still fail expert review because a definition is too narrow, a hypothesis is vacuous, or an unproven step has been promoted to an axiom.
\Cref{tab:taxonomy} lists the failure modes the statement review targets, grouped into four
families. Wrong-statement errors compile but state the wrong proposition.
Vacuity covers a concept defined as \texttt{True}, an unsatisfiable hypothesis,
and a witness that carries no real obstruction. Unproved shortcuts cover an unproven
step introduced as an \texttt{axiom} or through \texttt{sorry}, \texttt{admit}, or
\texttt{native\_decide}, and a load-bearing node mis-tagged \textsf{cited}{}.
Over-narrow statements cover dropped hypotheses and hardcoded constants that leave
the theorem narrower than claimed. Every entry type-checks; the kernel accepts all of
them.
\begin{table}[t]
\centering
\small
\caption{Failures that can pass the kernel while changing the intended claim.}
\label{tab:taxonomy}
\begin{tabular}{@{}p{0.15\textwidth}p{0.46\textwidth}p{0.31\textwidth}@{}}
\toprule
Family & Failure mode & How the review catches it \\
\midrule
Wrong statement & Type-checks but states the wrong proposition. & Per-node comparison with the intended claim. \\
Vacuity & Concept defined as \texttt{True}; unsatisfiable hypothesis; witness with no concrete obstruction; a trivially-true side collapsing a biconditional. & Witness normalization drops a witness with no obstruction; hypothesis-satisfiability check. \\
Unproved shortcut & Unproven step as \texttt{axiom}; \texttt{sorry}/\texttt{admit}/\texttt{native\_decide}; load-bearing node mis-tagged \textsf{cited}{}. & Mechanical scan for forbidden proof shortcuts; source check for borrowed nodes. \\
Over-narrow statement & Dropped hypothesis; hardcoded constant where general was intended; over-narrow model class. & Comparison with the intended claim; unused-hypothesis lint. \\
\bottomrule
\end{tabular}
\end{table}
Two layers perform the checking. A mechanical scan rejects any
completed artifact---and the closure of library modules it touches---that contains
\texttt{axiom}, \texttt{sorry}, \texttt{admit}, \texttt{native\_decide}, \texttt{opaque}, or
\texttt{unsafe}, and a build gate rejects any artifact with an open proof state.
By focused review, several agents read the \textsf{Lean~4}{} declaration text extracted from
the compiled file, compare it against the intended statement, and mark \texttt{drift}
on any divergence; the review requires every claimed witness to carry a concrete obstruction
and every \textsf{cited}{} node to have a real source match before final recording. A
reviewer does not compare the two surface forms directly: it first back-translates the
intended claim into a Lean-shaped hypothesis list and conclusion and then compares
that against the declaration, following the roundtrip and back-translation checks of
the autoformalization literature~\citep{roundtrip2026,backtrans2024}. No
surface-overlap score is used as evidence of a match, a use that literature
rejects~\citep{bleu_disavow2024}.
After the proof obligations are closed, a dual-model convergence reviewer rechecks
the full frozen graph, including nodes outside the current change frontier. This review
independently rechecks every statement against the intended claim before the result enters the
presentation stage. It is therefore the final gate in \Cref{fig:pipeline}.
\subsection{Library feedback}
\label{sec:pipeline-study}
The graph also controls what the pipeline carries forward after a run. \textsc{CausalSmith}{}
grows through two feedback channels: a run record that preserves what has been
attempted, and a verified library that grows with what has been proved.
The run record preserves every run at every disposition, from accepted to
rejected, together with its proposal, typed core, and review verdicts
(\Cref{tab:funnel,app:pipeline-record}). Before a new proposal is drafted, the
reconnaissance stage searches these records for open gaps and near-duplicates, and the
novelty-and-duplication gate compares a fresh proposal against prior entries. Failed
and downgraded runs contribute alongside accepted ones: a documented rejection
prevents a later run from repeating the same dead end, and a downgraded result
sharpens the novelty target for a related question. Because every run contributes
evidence, subsequent discovery starts from an accumulating record of successful and
unsuccessful attempts.
The library channel closes the loop for load-bearing lemmas. When the graph identifies
a missing lemma---a \textsf{gated}{} node that remains unproved and unsupported by the
current library---the pipeline can prove and promote the lemma to \textsc{Causalean}{}. A
library builder executes a bounded \texttt{study} workflow: a scaffolder creates a plan and a
file with proof obligations; parallel proof-filling agents resolve the obligations
against the live compiler; and a reviewer assesses whether the resulting lemma is generic,
reusable, non-vacuous, and \texttt{sorry}-free. A build gate confirms this assessment.
Promotion uses a verify-or-rollback procedure: the builder snapshots the library,
places the lemma in its appropriate module (merging it with existing declarations
when appropriate), and executes the integration chain---build, re-index, re-embed,
lint, and regenerate documentation. Any failure restores the snapshot; only a clean
integration is retained. Together, the two channels expand what the pipeline knows
(the run record) and what it can reuse (the library), and jointly reduce the burden of
subsequent runs.
\subsection{Presentation}
\label{sec:pipeline-papersmith}
The presentation stage consumes the reviewed graph. It converts an accepted result
into a working paper in which each theorem, definition, and assumption links to its
verified \textsf{Lean~4}{} source. Linking prose to code is established
practice~\citep{leanarchitect2026}. The
link records both facts attached to a graph node: the \textsf{Lean~4}{} object compiles, and the
statement has been marked \texttt{matched} to the English claim. An equivalence check
applies the criterion of \Cref{sec:pipeline-audit}: the paper statement and the \textsf{Lean~4}{}
declaration must express the same proposition, with neither stronger nor weaker than
the other. The check runs before the draft is revised. On failure, the pipeline
stops for human adjudication and preserves the intended declaration target.
\section{Results}
\label{sec:eval}
Our evidence is what the system produced, drawn entirely from the pipeline's
run records, logs, and library index. We give the distribution of outcomes across
runs, report which kinds of self-proposed question the system converts into accepted
results, examine one accepted result in depth, report the axiom audit that screens each
accepted result, and trace the library feedback loop closing on a concrete lemma. We
treat each as evidence for a claim in \Cref{sec:intro} and defer the more demanding
experiments---precision and recall of the audit, cost accounting, and an independent
significance panel---to future work. The pipeline also attaches a research-quality
signal to each result: an adversarial novelty gate assigns a tier, and the
presentation stage scores the finished write-up. These are LLM judgments of exactly
the kind this paper argues is unreliable (\Cref{sec:intro}), so we report them
without treating them as a validated evaluation of significance;
\Cref{sec:discussion} discusses why validating them is itself an open problem.
\subsection{The run catalogue}
\label{sec:eval-catalogue}
The run record holds $123$ runs, distributed across three dispositions
(\Cref{tab:funnel}). A run is accepted only when it is sound, novel at its
requested tier, and proved to completion in \textsf{Lean~4}{}; nine runs meet this bar. The
remaining runs are retained rather than discarded: as \Cref{sec:pipeline-study}
describes, downgraded and failed runs feed the record that screens later proposals.
\begin{table}[t]
\centering
\small
\caption{The run catalogue: $123$ recorded \textsc{CausalSmith}{} runs by disposition. A
separate literature-reproduction track adds one reproduced partial-identification
result. Counts are entries in the run record; a re-run that supersedes an earlier
attempt at the same question counts separately, and ten legacy runs from the
retired proposal track that predates the current pipeline are excluded.}
\label{tab:funnel}
\begin{tabular}{@{}lrl@{}}
\toprule
Disposition & Runs & Gate that determined it \\
\midrule
Accepted & $9$ & sound, novel at tier, proved in \textsf{Lean~4}{} \\
Downgraded & $44$ & sound, below the novelty target \\
Failed & $70$ & rejected at the proposal or the mathematics \\
\midrule
Total & $123$ & \\
\bottomrule
\end{tabular}
\end{table}
The nine accepted results span causal discovery, statistical and causal estimation,
panel methods, and experimentation; identification and structural-causal-model
results appear only in the lower tiers. The contrast with the size of the library
(\Cref{sec:library}) is worth stating plainly: although \textsc{Causalean}{} holds thousands
of machine-checked declarations, the number of fully accepted novel
discoveries is small. The evidence therefore supports the proposed
mechanism---kernel-checked proofs paired with graph-localized statement review---but
assessing discovery performance across causal inference will require a larger
evaluation.
\subsection{Which self-proposed questions the system converts}
\label{sec:eval-question-type}
The runs also carry a signal about what the topic selector is good at asking, not only
about how often it succeeds. Discovery assigns every run to one of six clusters before
any mathematics is attempted, so the assignment is fixed independently of the outcome.
Sorting the catalogue by cluster (\Cref{tab:by-cluster}) leaves the accepted results
concentrated in \texttt{Stat}, \texttt{Experimentation}, and \texttt{Panel}, and nearly
absent from \texttt{ExactID}, \texttt{PartialID}, and \texttt{SCM}, where $94$ runs produced
a single acceptance. The rule the split follows is not the clusters' subject matter,
which is broader than any one kind of result, but where in a run the difficulty falls.
A run in the first group typically takes an estimand whose identification is settled
and has to establish something analytical about it; a run in the second has to produce
the identification argument itself. The first kind of question can be posed against a
known quantity; the second cannot.
\begin{table}[t]
\centering
\small
\caption{The run catalogue by the cluster Discovery assigned at proposal time.
``Accept rate'' is accepted runs over total runs in the cluster. The rule dividing
the two blocks is described in the text; it is our reading of where the difficulty
of a run falls, not part of the clusters' definitions. Eight of the nine accepted
results fall in the upper block.}
\label{tab:by-cluster}
\begin{tabular}{@{}lrrrrr@{}}
\toprule
Cluster & Acc. & Down. & Fail. & Total & Accept rate \\
\midrule
\texttt{Stat} & $4$ & $7$ & $4$ & $15$ & $27\%$ \\
\texttt{Experimentation} & $3$ & $3$ & $1$ & $7$ & $43\%$ \\
\texttt{Panel} & $1$ & $0$ & $6$ & $7$ & $14\%$ \\
\midrule
\texttt{ExactID} & $1$ & $8$ & $27$ & $36$ & $3\%$ \\
\texttt{PartialID} & $0$ & $24$ & $30$ & $54$ & $0\%$ \\
\texttt{SCM} & $0$ & $2$ & $2$ & $4$ & $0\%$ \\
\midrule
Total & $9$ & $44$ & $70$ & $123$ & $7\%$ \\
\bottomrule
\end{tabular}
\end{table}
Reading the accepted topics themselves sharpens the pattern beyond the cluster labels.
Each of the nine names a specific published result and closes a technical gap
that the literature has already located; the targets include a matching anisotropic-H\"older converse to a
published higher-order-influence-function upper rate; the $\log^2$ gap of
\Cref{sec:eval-flagship}; a differentially private counterpart of a known conditional
average treatment effect rate; a two-sided welfare-regret rate under decaying overlap;
a demonstration that a published semidefinite design's Gaussian rounding certificate is
one-sided rather than exact; a matched Chebyshev lower bound for a rollout design; and,
in the one accepted identification run, a proof that a published order-$(2m{+}3)$
cumulant test for causal direction is not minimal, the direction being generically
recoverable one order lower. In each case the target was well posed before the run
began, and success was checkable against a published quantity.
The unsuccessful runs fail differently, and the run record says how. The recorded
downgrade reasons in the identification clusters repeatedly report a sound derivation
whose content collapses into an existing construction: reviewers describe the
delivered result as ``generic Manski-style outer containment,'' ``standard finite
response-type sharpness,'' ``shallow two-point mean-completion sharpness,'' or a
``one-line bookkeeping transfer.'' These runs were not stopped by an unprovable step
or an unfinished formalization. They were stopped because the mathematics, once
derived, turned out to be a known idea in new notation. The binding constraint in
these clusters is conception rather than proof.
A plausible mechanism is that the two kinds of question differ in how well posed they
are at proposal time. A technical gap supplies the proposer with a target and the
gates with a criterion: the converse must match the published upper bound, the
estimator must attain the stated rate, the test must use one fewer cumulant order.
The pipeline can grade partial progress against that criterion, and the run either
reaches it or visibly does not. A question whose contribution must be a new
identifying idea or a new framing supplies no such target. The proposer can state a
plausible-sounding object and pass the proposal gate, and only the derivation review
discovers that the object reduces to something known---by which point the run has
consumed its budget. This is consistent with the observation that the identification
clusters produce many downgrades rather than many outright refutations.
We report this as an observation about the current system, not a claim about
capability limits, and it is uncontrolled in three ways. The clusters differ in the topic
mix the selector proposed and in the novelty tier requested, so the comparison is not
between matched questions. \textsc{Causalean}{}'s coverage is deeper in estimation and
statistical theory than in partial identification (\Cref{tab:coverage}), so library
support and question type are confounded; a run that needs a new bound construction
also tends to need new substrate. And the accept/downgrade boundary is set by the
pipeline's own novelty gate, an LLM judgment of exactly the kind
\Cref{sec:discussion} declines to treat as validated. Separating question type from
library support---by proposing matched technical and conceptual questions within a
single cluster---is the experiment this observation calls for and that we have not run.
\subsection{A flagship result: closing a minimax gap for the ATE}
\label{sec:eval-flagship}
The strongest accepted result closes a standing gap in the minimax theory of
average-treatment-effect (ATE) estimation under high-dimensional discrete
confounding. \citet{zeng2024discrete} established the minimax lower scale
$n^{-1}+\big(d/(n\log n)\big)^2$ for estimating the ATE from $n$ i.i.d.\ observations
$(X,A,Y)$ with a discrete confounder $X\in\{1,\dots,d\}$, binary treatment $A$ and
outcome $Y$, and strict-interior overlap $\epsilon\le\Pr(A=1\mid X=k)\le 1-\epsilon$.
The estimators they analyze, however, leave a $\log^2$-factor gap between the known
upper and lower bounds. The run constructs a single computable estimator that closes
it.
Under the stated overlap, consistency, and conditional-exchangeability assumptions,
the target is the adjustment functional
$\tau(P)=\sum_{k=1}^{d}p_k(\mu_{1k}-\mu_{0k})=\mathbb{E}[Y(1)-Y(0)]$, where
$p_k=\Pr(X=k)$ and $\mu_{ak}=\mathbb{E}[Y\mid A=a,X=k]$. The estimator splits the sample in two, uses a
pilot count to label each covariate cell heavy or light, and treats the two regimes
differently: heavy (well-populated) cells receive a plug-in ratio estimator, while
light (sparsely sampled) cells receive a best-polynomial approximation of the cell
functional with unbiased factorial-moment lifting. A single universal numerical
calibration---fixed constants that do not take the overlap $\epsilon$ as
input---controls the split, the polynomial degree, and the variance normalization,
and the estimator runs in $O(dM^4)$ arithmetic operations. The headline theorem
states that, for every fixed $0<\epsilon<1/2$, this estimator attains
\[
\mathsf R_{n,d,\epsilon}\;\asymp_\epsilon\;
\frac1n+\Big(\frac{d}{n\log n}\Big)^2
\qquad\text{uniformly for } d\lesssim_\epsilon n\log n,
\]
so the minimax MSE has parametric order $n^{-1}$ whenever $d=O(\sqrt n\log n)$ and
tends to zero if and only if $d=o(n\log n)$. It is formalized as
\texttt{sharp\_minimax\_fixed\_interior} across twenty-six \textsf{Lean~4}{} modules, together
with the light-cell approximation lemma, the heavy-cell aggregation bound, the
universal-tuning corollary, and a verified two-category confounding witness.
The logic graph records the scope of the contribution and makes the boundary
auditable. The novel, proved part is the upper bound: the hybrid
estimator and its matched rate. The minimax lower half is not reproved here;
it is transferred from the published moment-matching bound of
\citet{zeng2024discrete}. In the \textsf{Lean~4}{} development this borrowed bound appears as
an explicit hypothesis on the headline theorem---a \textsf{cited}{} node carrying its
source---rather than an \texttt{axiom} inserted into the proof. This follows the
borrowed-result discipline of \Cref{tab:taxonomy}: a load-bearing external result is
carried as a typed hypothesis with source evidence, so a reader sees precisely which
part is proved in this work and which is imported. The result was accepted at the
field-novelty tier.
\subsection{Machine-checked soundness}
\label{sec:eval-axiom-checks}
Each accepted result is screened for the unproved-shortcut failures of
\Cref{tab:taxonomy} before it is recorded. In a clean build, \texttt{\#print axioms} is
run on the headline theorem and cross-checked by a comment-aware scan of the recorded
module and its reachable library closure for \texttt{sorry}, \texttt{admit},
\texttt{native\_decide}, and \texttt{axiom} (\Cref{app:repro}). For the flagship result,
the twenty-six modules of the development contain none of these, and the headline
theorem reduces to \textsf{Lean~4}{}'s standard axioms; its single external input, the
\citet{zeng2024discrete} lower bound, is visible as a hypothesis, not an axiom. This
is what separates a kernel-accepted proof that rests only on its stated assumptions
from one that has quietly promoted an open step to an \texttt{axiom}.
\subsection{Library feedback in action}
\label{sec:eval-selfimprove}
The library feedback loop can be traced through a complete instance. Proving the
converse half of a dose-response result from another accepted run required a
Bretagnolle--Huber affinity bound for arbitrarily many hypotheses, absent from
Mathlib. The library builder proved this result and
promoted it to \textsc{Causalean}{} as
\texttt{Causalean.Stat.}\allowbreak\texttt{bretagnolle\_huber\_affinity}; a subsequent
result, the Le Cam two-point reduction on which the converse depends, now imports and
reuses it. Thus a run required a lemma, the system proved it, promotion added it to
the library, and a later result consumed it. Thirteen library builds have produced
such promotions, including Fano's inequality, a KL density-tilt expansion, and
Chebyshev design tools. Estimating how library growth trades off against cost per
result remains future work (\Cref{sec:discussion}).
\section{Discussion and Limitations}
\label{sec:discussion}
\textsc{CausalForge}{} separates three questions. First, the \textsf{Lean~4}{} kernel checks that a
proof is valid. Second, the statement audit checks node by node whether each formal
statement expresses the intended claim; this review can still miss errors. Third, the
importance of a final paper remains a human judgment, informed by the pipeline's
novelty tiers but not determined by them. Keeping these questions separate prevents a
valid proof from being mistaken for a meaningful or important result. The pipeline machinery is largely domain-independent, whereas the formal library is
specific to causal inference. Applying the approach to another field requires building
or adopting a comparable library and retrieval interface. The graph, audit, and
library feedback loop should transfer with limited modification.
Our reporting has several limitations, the first of which concerns research quality.
The pipeline estimates it: an adversarial novelty gate assigns tiers and the
presentation stage scores each write-up. But these are LLM judgments, and the
independent human evaluation that would validate them is absent. We therefore report
what the system produced and how the pipeline rated it, not an established measure
of significance. Building such a measure is itself an open problem: unlike proof
soundness, which the kernel decides, or statement match, which reduces to a local
comparison, the value of a correct theorem resists the labeled ground truth a
benchmark requires. We regard constructing such a benchmark, and convening an
independent panel, as future work. Second, the faithfulness audit itself relies on an
LLM. The task it poses is narrower than open-ended review, and frontier models
performed well on it in our observations, but a model can still err when auditing a
statement, and we do not estimate how often it does. Third, the cost and reuse evidence is qualitative because the runs record iteration
depth but not token use or elapsed time, and the accepted catalogue is small and
concentrated in estimation and experimentation.
\section{Conclusion}
\label{sec:conclusion}
Automated theoretical research requires a reliable basis for evaluating correctness,
yet LLM reviewers can be misled. We have described a causal-inference system that
uses formal verification to establish proof soundness while making the limits of its
other assessments explicit. A verified library reduces formalization cost; a
topic-selecting, graph-audited pipeline proposes and proves results while assessing whether each
statement expresses its intended claim; and a library feedback stage expands the
library with lemmas required by completed runs. The resulting trust model has three
parts: the kernel checks the proof, the statement audit checks each formal statement
against the intended claim, and significance remains a human judgment. The principal next
steps are a rigorous study of audit reliability, controlled ablations against
kernel-only and LLM-judge-only baselines and an independent novelty panel provied from expert judgement.
\bibliographystyle{plainnat}
\bibliography{references}