CausalForge用Lean做因果推理自动研究，能验证证明并审计陈述，比纯LLM评审靠谱。
CausalForge是一个基于Lean证明助手的自动化因果推理研究框架。它结合了CausalLean库（含7,035个机器验证声明）和CausalSmith自改进智能体管道。该框架通过机器验证证明和语句审计，解决了LLM评审在2025年Bad Scientist研究中被指出的不可靠问题（接受伪造论文的概率接近随机）。已完成自主研究运行，并在GitHub公开源码、库和运行记录。
CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
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 (Bad Scientist, 2025). We present CausalForge, a framework for automated theoretical research in causal inference grounded in the Lean proof assistant. CausalForge combines 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 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 https://github.com/Jiyuan-Tan/CausalForge.