CausalSmith uses Lean proofs to make self-improving agents automate causal research
skoularidou · x · 2026-09-16
- The CausalSmith paper (Jiyuan Tan, Vasilis Syrgkanis) proposes a Lean-proof-assistant-based framework for automated theoretical research in causal inference, tackling the problem that LLM reviewers accept fabricated papers and catch fabrication at near-chance rates.
- Core idea: proofs are checked by a program rather than read by a referee. The authors built Causalean, a foundational Lean library for causal inference with 8,179 machine-checked definitions and theorems, developed with LM assistance under human design and review.
- Around it runs a self-improving agentic pipeline that selects topics, proposes results, formalizes statements, constructs proofs, and presents artifacts for human inspection; Lean verification is paired with a statement audit comparing each formal theorem against its informal claim.
- Evaluated on artifacts from completed autonomous research runs; source code and the formal library are open.
Related event: CausalSmith: Lean-Verified Causal Inference Research by AI Agents(2 posts)→
More from coding & agent
- Lean Kernel Challenge Stage 1 launches to speed up verified computation in the Lean 4 kernel — AlexKontorovich · 2026-09-16
- Lean Kernel Arena benchmarks 20+ kernel checkers, some 4x faster than official — AlexKontorovich · 2026-09-16
- Celesto gives computer-use agents disposable full macOS desktops on Apple Silicon via Lume — aniketmaurya · 2026-09-16
- Reverse engineering in 2026: hand the agent a goal, walk the dog, come back to a perfect IDB — dyn___ · 2026-09-16
- Jev model claims 40-400x cheaper than Gemini; dev backtest finds it faster and more consistent — FrankFelixAI · 2026-09-16
- Vibe coding feels like scrubbing 2015 Google results: steer agents away from the generic middle — _Stocko_ · 2026-09-16