Extracted main text — title through conclusion, appendix excluded. This is what our citation measures are computed over, published so the extraction can be checked by eye.
73,424 characters · 23 sections · 56 citation commands
CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
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 aiscientist2025 report hallucinated numbers, frequent coding failures, and little genuine novelty aiscientist_eval2025. More concerningly, 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 Lean 4 and its proof is accepted by the kernel, the proof is guaranteed to be correct relative to 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 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 sorry and still be mathematically uninformative: a definition may reduce to True; or an unproven step may be introduced as an axiom that the kernel accepts. Recent work documents this gap from several angles sorries2026, signalcoverage2026,beyondkernel2026, and we observed it in our own runs as well. In one, an agent converted difficult lemmas into axioms, yielding a type-checking shell with axioms substituting for proof. In another, the model altered a hypothesis, so the 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 ((ref)) that compares each formal statement with the claim it is meant to express, so that the 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 CausalForge, which has two components. Causalean is a 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 Lean 4 statements. 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 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.}
\paragraph{Availability.} The Causalean library, the CausalSmith pipeline, and the run record backing (ref) 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.
(ref) places 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. CausalForge contributes the combination of proposing a causal theorem and auditing that its formal statement means what was claimed.
\paragraph{Autoformalization, theorem proving, and statement matching.} A large body of work uses language models with proof assistants, from neural proof search gptf2020,htps2022 and early autoformalization wu2022autoform,dsp2022 to whole-proof generation and repair baldur2023, retrieval-augmented provers leandojo2023,deepseekprover2025, and competition-level systems alphageometry2024,alphaproof2025. These systems are usually measured on benchmarks of known problems, including MiniF2F, ProofNet, and PutnamBench 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---sorry-free formalizations still fail expert review sorries2026, type-correct statements can be semantically wrong signalcoverage2026,beyondkernel2026, and vacuity and reward hacking are common enough to benchmark formalreward2026. Proposed remedies include roundtrip and back-translation equivalence checks faithfulnessgap2026,roundtrip2026,backtrans2024, learned alignment scorers between a statement and its formalization formalalign2025, and a rejection of surface-overlap metrics as evidence of a correct statement match 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 leanarchitect2026,proofflow2025. The broader shift toward proof-assistant-grounded reasoning 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 aiscientist2025 are vulnerable when an LLM judges their output, whether by independent re-evaluation aiscientist_eval2025 or by adversarial construction badscientist2025. A complementary tradition grounds discovery in a hard verifier---program search against a fitness function 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 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 ma2025causal. Benchmarks measure whether models answer causal queries or choose valid research designs---CLadder and Corr2Cause on graphical and correlational reasoning cladder2023,corr2cause2024, CaLM and QRData on broad and data-grounded causal question answering 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 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 gao2023chatgptcausal, recite memorized causal facts rather than reason interventionally causalparrots2023, commit elementary causal fallacies fallacies2024, and are flattered by benchmarks solvable through knowledge lookup causalreview2024. A third strand builds agents that do causal analysis, automating discovery, data preparation, and estimator selection but offering no correctness guarantee 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 causalaiscientist2026, LLM-assisted search for instrumental variables miningcausality2024, and the multi-agent IV Co-Scientist 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 leancopilot2024 and to the causal-LLM line above, which does not provide formal verification. CausalForge addresses this intersection.
\paragraph{The closest related systems.} Two efforts are particularly closely related. A Lean library for economics econcslib2026 formalizes established economic theory, and a multi-agent system formalizes asymptotic statistical theory with auditor and reviewer agents that already guard against vacuity asymptoticstats2026. 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.
\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. Causalean ((ref)) formalizes most classical results under these frameworks.
\paragraph{Lean 4 as a proof checker.} Lean 4 is an interactive theorem prover and programming language in which mathematics is written in a fully formal language 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 tactics---commands such as intro, simp, or 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 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 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 (ref) takes up.
The cost of formalizing results from first principles limits automated discovery, and Causalean supplies the reusable foundation that discovery needs. It is a foundational 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.
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 (ref).
The library was built with LLM assistance rather than written by hand, and the division of labor follows the trust model of (ref). 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 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 ((ref)). 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 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 ((ref)).\footnote{These repository statistics are a snapshot. The totals may increase because the CausalSmith pipeline runs continuously and can promote newly proved, reusable declarations to Causalean.} Ten clusters cover the field from graphical foundations to asymptotic statistics.
The library layers from graphical and measure-theoretic foundations up to the estimation and design methods that depend on them ((ref)).
\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.
The library also provides a collection of classical flagship results from the literature. (ref) catalogues the principal substantive result families across the library's major research areas. Each entry is a named declaration with a machine-checked proof; (ref) 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.
A library of this size requires effective declaration retrieval, so retrieval is a primary component of 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 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.
The library passes the axiom checks required for its use as a verified foundation. All $7{,}035$ declarations are sorry-free, and the corpus is free of hand-written axiom; the only non-standard axioms are compiler artifacts introduced by native_decide, which occur in finite-graph decidability arguments and several minimax calculations and are reported explicitly. Two results are not original to Causalean but adapted, re-licensed copies of external Lean 4 developments, bumped to 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} 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} 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 ((ref)). \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.
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 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 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, 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. (ref) summarizes the workflow; (ref) give an operational specification of the stages, artifacts, recovery rules, and presentation workflow.
Dependency graphs for proofs are established practice; Lean blueprints and proof-flow tools represent developments as DAGs of statements leanarchitect2026, proofflow2025. 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 Lean 4 declaration, a review status in $\{\texttt{unreviewed}, \texttt{matched}, \texttt{derived}, \texttt{drift}\}$ recording the current statement match, and a class: a gated node represents substrate missing from Causalean and must be discharged by a proof before the result can be recorded as complete, while a 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, statement-uses and 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 ((ref)).
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 Lean 4 declarations. Proof construction adds the proof dependencies. Statement matching changes review statuses such as matched or drift. Presentation then uses the reviewed graph as the source of truth for the paper-to-code crosswalk. The critical path consists of gated nodes: a result is complete when every gated node has a proof and is marked matched. When a statement changes, the pipeline returns that node to unreviewed and rechecks the affected frontier and its dependents.
The pipeline supports two entry modes. A researcher may supply a topic anchor, or the main orchestrator may invoke the 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 Lean 4 declaration, a module location, and either a proof obligation or a reuse target from 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 (ref) to reuse existing results. A deterministic lint flags hypotheses unused by the proof, which may indicate a vacuous or mis-stated theorem.
The statement-match gate in (ref) is the statement faithfulness audit. The Lean 4 kernel establishes proof soundness, but, as (ref) 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 True, or a lemma asserted as an 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 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 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.
(ref) 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 True, an unsatisfiable hypothesis, and a witness that carries no real obstruction. Unproved shortcuts cover an unproven step introduced as an axiom or through sorry, admit, or native_decide, and a load-bearing node mis-tagged 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.
Two layers perform the checking. A mechanical scan rejects any completed artifact---and the closure of library modules it touches---that contains axiom, sorry, admit, native_decide, opaque, or 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 roundtrip2026,backtrans2024. No surface-overlap score is used as evidence of a match, a use that literature rejects 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 (ref).
The graph also controls what the pipeline carries forward after a run. 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 ((ref)). 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 gated node that remains unproved and unsupported by the current library---the pipeline can prove and promote the lemma to Causalean. A library builder executes a bounded 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 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.
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 Lean 4 source. Linking prose to code is established practice leanarchitect2026. The link records both facts attached to a graph node: the Lean 4 object compiles, and the statement has been marked matched to the English claim. An equivalence check applies the criterion of (ref): the paper statement and the 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.
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 (ref) 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 ((ref)), so we report them without treating them as a validated evaluation of significance; (ref) discusses why validating them is itself an open problem.
The run record holds $123$ runs, distributed across three dispositions ((ref)). A run is accepted only when it is sound, novel at its requested tier, and proved to completion in Lean 4; nine runs meet this bar. The remaining runs are retained rather than discarded: as (ref) describes, downgraded and failed runs feed the record that screens later proposals.
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 ((ref)) is worth stating plainly: although 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.
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 ((ref)) leaves the accepted results concentrated in Stat, Experimentation, and Panel, and nearly absent from ExactID, PartialID, and 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.
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 (ref); 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. Causalean's coverage is deeper in estimation and statistical theory than in partial identification ((ref)), 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 (ref) 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.
The strongest accepted result closes a standing gap in the minimax theory of average-treatment-effect (ATE) estimation under high-dimensional discrete confounding. 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 sharp_minimax_fixed_interior across twenty-six 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 zeng2024discrete. In the Lean 4 development this borrowed bound appears as an explicit hypothesis on the headline theorem---a cited node carrying its source---rather than an axiom inserted into the proof. This follows the borrowed-result discipline of (ref): 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.
Each accepted result is screened for the unproved-shortcut failures of (ref) before it is recorded. In a clean build, \#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 sorry, admit, native_decide, and axiom ((ref)). For the flagship result, the twenty-six modules of the development contain none of these, and the headline theorem reduces to Lean 4's standard axioms; its single external input, the 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}.
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 Causalean as Causalean.Stat.\allowbreakbretagnolle_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 ((ref)).
CausalForge separates three questions. First, the 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.
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.