Causalean Library
- Declarations
- 15,824
- Sorry-tainted
- 0
The foundational Lean 4 library for causal inference that every paper on this site builds on. Each declaration carries a natural-language translation — the first paragraph of its docstring. Every formal statement here is machine-checked; the translation beside it is prose, so it is separately confirmed by a human against the formal statement. Translations still awaiting that confirmation are flagged to review, so you can see exactly which prose has not yet been checked.
Dependency graph
An edge X → Y means Y’s formal statement mentions X: arrows run from building blocks to the results that use them. Explore by module, then declaration; read arrows backward to trace a result’s prerequisites. Drag a node to pin it, and double-click to release it.
Loading dependency graph…
| Module | What it provides | Declarations | To review | Sorried |
|---|---|---|---|---|
| Discovery | Causal discovery: LiNGAM identifiability, linear disentanglement, and invariant prediction tools for recovering structure from distributional and environment-shift information. | 285 | — | — |
| Estimation | Estimation and inference for causal estimands: orthogonal moments and double machine learning, influence functions and asymptotic normality, efficiency bounds, cross-fitting, CATE learners, NPIV, and rate/coverage-facing results. | 1,278 | — | — |
| Experimentation | Design-based experimentation under interference: finite randomization designs, exposure mappings, Horvitz-Thompson estimators, variance bounds, consistency, CLTs, and paper-specific Aronow-Samii, Hudgens-Halloran, and Savje-Aronow-Hudgens results. | 611 | — | — |
| Graph | Causal graphs: DAGs, d-separation via Bayes-Ball, SWIGs and their splits, and c-components. | 465 | — | — |
| ML | Standalone, causal-free supervised-learning library: basic regression methods (linear least squares and series/sieve, ridge, lasso, L²-ball ERM rates, logistic, kernel ridge, feedforward networks, finite-partition predictor ensembles) as first-class objects, each with its defining-optimization, closed-form/structure, and population-target properties. It also provides proper and strictly proper binary losses with their population minimizers. Built on a dual-view spine (a parametric predictor and an extensional hypothesis class joined by a bridge). Imports nothing from the causal layers. | 179 | — | — |
| Mathlib | Mathlib-shaped helper lemmas staged for upstreaming: conditional distributions, conditional independence, and integration gaps. | 4,124 | 2 | — |
| PO | Standard potential-outcome framework for econometric causal inference: PO systems, variables and bundles, consistency, counterfactual distributions, and the conditional-independence assumptions used in identification. | 1,847 | — | — |
| Panel | Panel-data causal econometrics: adoption paths, cell-level potential outcomes, fixed effects, residualization and weighted-regression infrastructure, and estimand-characterization results for DiD, event-study, and TWFE designs. | 636 | — | — |
| SCM | Structural causal models: the CausalModel core, factored kernels, do-calculus rules, and the Markov layer connecting graphs to distributions. | 830 | — | — |
| Stat | Statistical foundations: convergence modes, limit theorems, concentration inequalities, and minimax lower-bound tools. | 5,569 | 1 | — |
Machine-readable index: search.json ·
full index at doc/library_index.json in the repository.