CausalSmith is an autonomous system that discovers a causal-inference result, formalizes it, proves it in Lean 4, and writes it up as a paper — with every formal statement machine-checked by the proof kernel and audited to mean what it says. This page walks through the pipeline end to end, mostly in pictures.
Language models now generate conjectures, proofs, and whole papers far quicker than anyone can evaluate them. In theory work an incorrect theorem can look exactly like a correct one until it is verified — and the popular fix, letting one model review another, is not a reliable correctness oracle.
Formal verification offers a different footing. When a proof is accepted by Lean's kernel, it is valid relative to a small trusted core — a guarantee no LLM reviewer can give. CausalSmith is built around making that guarantee cheap, and around the one thing the kernel still cannot check.
"Is this good research?" bundles three very different questions. CausalSmith pulls them apart, and handles each where it can actually be handled.
Eliminated by construction: the Lean kernel mechanically checks every step against its trusted core.
The kernel does not give you this. It is audited node by node — a small, local, re-checkable comparison, not a certificate.
Not guaranteed by either of the above. It stays an explicit human judgment — the pipeline never pretends otherwise.
The whole design shrinks the residual judgment from the open-ended "is this valuable research?" to the bounded "does this Lean statement match this English claim?"
A result moves left to right through four stages, clearing a gate between each. Two feedback loops make the system improve itself: it reuses a verified library and grows it, and it records every run so the next proposal starts from what has already been tried.
The pipeline. Amber pills are the gates a result must clear; the green library below feeds reuse into Formalize and receives proven lemmas back through study mode; the run bank records every run and feeds reconnaissance before the next proposal.
sorry, or a smuggled axiom gets through.Those four stages expand into a deterministic state machine. Each stage either advances or, through a gate (amber), returns work to the stage before it; four checkpoints (red) halt the run for an external decision. The inset zooms into the F2–F4 proof-and-faithfulness loop: a scaffold mismatch returns to F2, while a blocking lint or failed convergence review re-enters at F2.5; a genuinely false claim from F2.5 or F3 escalates out to the mathematics rather than being quietly rewritten to pass.
The operational stage flow of one theorem run. Discovery (top) produces a proposal and typed core, frozen at D0.5 and handed through the D/F checkpoint to Formalization; amber gates return work to the preceding stage and red checkpoints mark run halts for external judgment. The green band details the bounded F2–F4 loop the kernel-checked proof runs inside.
A result is stored as a logic graph: nodes are statements — a setup, a definition, an assumption, a lemma, the headline theorem — and edges record dependencies. This turns the global question "is this proved and faithful?" into a per-node one, so a change re-opens only the nodes it touches instead of the whole paper.
A logic graph (schematic). Fill encodes review status; a dashed blue border marks a borrowed cited node off the critical path. The green underlay traces the critical path of gated nodes the audit must clear before the result is banked.
A development can be free of sorry and still be uninformative. The audit
targets four families of failure — every one type-checks, so the kernel accepts them all.
Type-checks but states the wrong proposition. Caught by a per-node statement ↔ claim match.
A concept defined as True, an unsatisfiable hypothesis, or a witness with no real obstruction — the theorem holds emptily. Caught by witness normalization and a hypothesis-satisfiability check.
An unproven step slipped in as an axiom, sorry, or native_decide; or a load-bearing node mis-tagged as merely cited. Caught by a mechanical cheat-token scan and gated-vs-cited attestation.
A dropped hypothesis or a hardcoded constant leaves the theorem narrower than claimed. Caught by a statement gate and an unused-hypothesis lint.
Mechanical scans, an independent reviewer with fresh context, and a human adjudicator at load-bearing checkpoints keep the auditor from sharing the blind spots of whatever produced the statement.
Formalizing from first principles is slow, so the pipeline composes a foundational Lean library of causal inference rather than re-deriving results. It layers from graphical and measure-theoretic foundations up to the estimation and design methods on top, with a retrieval index spanning the whole stack — the interface agents query to reuse a result instead of reinventing it.
Causalean in layers: foundations support the model languages, which support identification, which supports the methods on top. One retrieval index over all declarations spans the stack and is what the pipeline queries.
sorry
Nothing in the library relies on sorry and it contains no hand-written
axiom. A few flagship results give a sense of its depth:
backdoor_identifiable_ae frontdoor_identifiable_ae id_sound_discrete late_wald att_csdid balkePearl_sharp dml_ATE_attains_hahn_bound uStatisticOrder_clt localDependenceCLT_of_stein Two feedback channels compound over time, so each run leaves the pipeline better equipped for the next.
Every run is stored — its proposal, typed core, verdicts, and disposition — whether accepted, downgraded, or rejected. A documented dead end stops a later run repeating it; reconnaissance mines the bank before the next proposal is drafted.
When a run needs a load-bearing lemma the library lacks, study mode proves it,
checks it is generic and sorry-free, and promotes it back into Causalean
under verify-or-rollback — where the next run can simply reuse it.
Autonomous research systems usually close their loop with an LLM judge over the open-ended question "is this good research?" — and that judge can be fooled. CausalSmith instead makes the proof correct by construction and confines the remaining judgment to a small, local, re-checkable question: does this Lean statement mean the intended claim? Formal verification is the correctness evaluator automated theoretical research was missing.