Recently, thanks to the rapid improvement of large language models (LLMs), there have been many breakthroughs on open problems in pure math. With the help of formal languages like Lean 4, LLMs can now check the correctness of their proofs without humans. For example, OpenAI claimed that their internal model solved the famous Navier–Stokes problem, one of the Millennium Prize Problems, and provided a Lean verification of the proof¹. OpenAI also claimed to lower the bound on gaps between primes to 186² and to solve several other open problems³. From these examples, we can see that LLMs have already proved their ability to produce high-quality research in math.

Can the same happen beyond pure math? In this work, we explore whether LLMs can automate theoretical research in applied science, in particular causal inference. Causal inference is the study of cause and effect. It asks whether one variable causes another, for example, whether a drug lowers blood pressure or whether a training program raises wages, and how large the effect is. Its theory tells us which assumptions make such a conclusion valid and how to estimate the effect. Causal inference is a good testbed for automated research. On the one hand, its results are precise theorems, just as in pure math. On the other hand, each theorem relies on a model of a real-world problem, so in addition to proving the theorem, one needs to choose assumptions that match the application.

We build an agentic pipeline, CausalSmith, to automate theoretical causal inference research. Both theorists and practitioners can benefit from the research produced by CausalSmith. For example, theorists can build on the new theorems, and practitioners can apply them to real problems. We first let LLMs propose ideas and write down their results in natural language for review. Then, another agent checks the results by formalizing them in Lean 4. To do this, we build Causalean, a Lean 4 library for causal inference, and then build the pipeline around it.

Figure 1. A result moves left to right through three stages and must pass a review (amber diamond) between them. Inside formalization, each statement is translated into Lean, audited against the paper, and proved. Causalean supplies known results and takes in new ones. The run bank keeps every attempt so that future runs can learn from it.

How does CausalSmith turn an idea into a verified result?

The pipeline has three stages (Figure 1): discovery, formalization, and presentation. In the first stage, it proposes new results and writes them down, together with their proofs, in natural language for another agent to review. The LLM reviewer then checks the correctness and novelty of the results. After the results pass the review, the formalization stage checks them in Lean, and the presentation stage produces a human-readable paper with an interactive web page.

To illustrate how the pipeline works, we take one of our accepted results as an example. In the discovery stage, the agent starts from a 2024 paper by Zeng et al.⁴ on estimating the average treatment effect under discrete covariates. The authors proved a lower bound for this problem, but the upper bound of their estimator does not match it, and they left closing the gap to future work. The agent then proposes a new estimator to close the gap and writes down the proof in natural language. Another agent checks the math and compares the result with the literature. In the formalization stage, the proof needs concentration bounds for random counts, which are not contained in Mathlib, Lean’s standard math library. Therefore, the pipeline proves these bounds, adds them to Causalean, and finishes the Lean proof. Finally, in the presentation stage, the result is turned into a paper with an interactive web page and a 20-minute slide deck.

Beyond a single run, we also have two feedback loops that improve the pipeline over time (Figure 2). First, all papers, whether they pass or fail, are stored in a run bank, so future runs can learn from both failed and successful attempts. Second, if the pipeline finds any reusable lemmas or theorems during a run, it derives their most general form and promotes them into the Causalean library. For example, the concentration bounds in the result above are promoted to Causalean, and the next accepted result on the same problem directly reuses them instead of proving them again.

Figure 2. Loop 1: every run goes into the run bank, together with the reason if it failed, and new proposals are screened against it. Loop 2: reusable lemmas proved during a run are generalized, checked, and promoted into Causalean, so later runs start from a bigger library. Run counts are taken from our project page as of October 2026.

Does it work?

As of October 2026, we have run CausalSmith 1,732 times in total. Each run ends with one of three outcomes. A run is accepted if its result is correct, fully proved in Lean, and novel enough (as judged by an LLM) to meet the bar set at the start of the run. Of all runs, 41 (2.4%) were accepted. A run is downgraded if its math is correct but the reviewer finds the contribution incremental, and 1,388 runs were downgraded. A run fails if its proposal or its math is rejected during the run, and 303 runs failed. Downgraded and failed runs are also stored in the run bank, so future runs can avoid the same mistakes.

Our featured result, “Sharp Minimax Rates for Average Treatment Effects with Discrete Confounding under Fixed Overlap,” is the one we used as an example above. It studies how accurately one can estimate the average treatment effect from n observations when the confounder takes d values and every group has a fixed minimum chance of receiving each treatment. Zeng et al. proved a lower bound on the error of any estimator, but no known estimator reached it. CausalSmith proposes a new estimator that closes this gap and achieves the minimax rate. We have manually checked the correctness of this paper and found that its proof uses some interesting techniques that have not been applied in causal inference before.

How does it stay honest?

One subtle point lies in formalization. While Lean guarantees the correctness of the math, it does not automatically check whether a Lean statement says the same thing as the natural-language claim. For example, an agent can quietly change a hypothesis and prove a weaker theorem than the paper claims. Therefore, the formalization stage has an auditing step that checks the faithfulness of every statement (Figure 3).

Figure 3. An overview of how the auditing step checks for faithfulness. (1) The pipeline stores each paper as a graph of definitions, assumptions, lemmas, and theorems. (2) A zoomed-in view of one theorem. (3) Its Lean version. The audit matches the two piece by piece, so that every assumption and the conclusion line up, with nothing added or dropped.

What is underneath? The Causalean library

Mathlib, Lean’s standard math library, provides basic definitions and theorems for proving new results, but it covers almost no causal inference. Without a causal inference library, one needs to formalize the basic definitions and theorems of causal inference on top of Mathlib for every new result, which makes the whole process time-consuming and costly. To address this limitation, we build Causalean, a Lean 4 library of classical results in statistics and causal inference. We first manually select commonly used results from the literature, design the structure of the library, formalize those results with LLM assistance, and manually review each statement. Then, starting from this base version, every later CausalSmith run builds on the library and, after careful LLM review, adds missing classical results back to it (the second loop described above). The library now holds more than 15,000 Lean-verified definitions and theorems, covering causal graphs, potential outcomes, structural causal models, estimation, experiments, and panel data. During the LLM review, the agent checks whether each Lean statement matches the textbook statement or paper it comes from. In addition, the reviewer checks that each lemma is general, reusable, and not vacuous.

Figure 4. Each circle is one part of the Causalean library, and the number is how many Lean-verified definitions and theorems it holds (snapshot from the project page, October 2026).

Human-AI interaction interface

With the help of this agentic system, one can easily produce a large number of results given enough budget. However, Lean only checks that the proofs are correct; whether a result is interesting or useful still needs human review. To make that review easier, we also explore new ways to present papers for better understanding and interaction. Our project page supports the following features, which help readers understand each paper and interact with the pipeline and with other researchers.

Ratings and comments. Every reader can rate a paper and comment on any part of it to exchange intuitions and thoughts. Readers can also certify the correctness of individual statements.

Figure 5. On the project page, readers can (1) rate a paper, (2) certify statements one at a time on the proof map, where green dots mark certified statements, and (3) comment on any passage.

Natural language–Lean matching. For most definitions and theorems, a click on the block shows the corresponding Lean statement, so anyone can check whether it matches the natural-language statement.

Figure 6. Clicking a statement in the paper opens the Lean declaration it was audited against, hypothesis by hypothesis.

Slides. Each paper comes with a 20-minute slide deck that illustrates its main idea and contributions.

Figure 7. Each paper comes with a slide deck. This slide shows the main result of our featured paper.

Citations. Each paper that passes the novelty review and Lean verification comes with its own DOI and citation. Anyone can cite these results in their papers.

Limitations and next steps

With CausalSmith, one can produce many results with a modest budget, so a natural question is how good the produced papers are. Currently, our pipeline mainly uses LLM reviewers to filter out bad ideas. As of October 2026, we have manually reviewed only a small portion of the produced papers, so we do not yet know their overall quality. For now, the ratings, certifications, and comments on the project page are the main way to collect human judgment, and we welcome readers to use them. One future direction is to develop more systematic novelty measures and to build a benchmark that evaluates the ability of LLMs to do novel research.

Paper: arXiv:2607.22511 · Project page: causalsmith.org

1. OpenAI (2026, September 8). On the Navier–Stokes Millennium Prize Problem. https://openai.com/index/navier-stokes-solution/ ↩

2. OpenAI. PrimeGaps186. GitHub repository. https://github.com/openai/PrimeGaps186 ↩

3. OpenAI. math. GitHub repository. https://github.com/openai/math ↩

4. Zeng, Z., Balakrishnan, S., Han, Y., & Kennedy, E. H. (2024). Causal Inference with High-dimensional Discrete Covariates. arXiv preprint arXiv:2405.00118. https://arxiv.org/abs/2405.00118 ↩