Pith. sign in

REVIEW 3 major objections 4 minor 56 references

CausalForge claims that automated causal-inference research becomes trustworthy only when kernel-verified proofs are paired with an audit that formal statements match intended claims, and it reports a machine-checked minimax rate that close

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 04:30 UTC pith:I3K5EXLF

load-bearing objection Worth a serious referee slot: the integration is genuinely new and the authors are unusually candid, but the advertised two-part guarantee rests on an LLM statement audit whose error rate is unmeasured. the 3 major comments →

arxiv 2607.22511 v1 pith:I3K5EXLF submitted 2026-07-24 stat.ML cs.AIcs.LGecon.EM

CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference

Jiyuan Tan , Vasilis Syrgkanis This is my paper
classification stat.ML cs.AIcs.LGecon.EM
keywords causal inferenceformal verificationLean 4automated theorem provingagentic research pipelinestatement faithfulnessminimax estimationaverage treatment effect
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

CausalForge is trying to establish that automated theoretical research in causal inference can be made reliable by separating two guarantees: the Lean 4 kernel checks that a proof is valid, and an explicit statement audit checks that the formal theorem says what the informal claim intended. A sympathetic reader should care because LLM review alone has been shown to accept fabricated papers, and CausalForge replaces that evaluation with a machine-checked kernel plus a node-by-node faithfulness audit over a logic graph. The system also tests whether discovery can be self-improving: it selects topics, grows a 7,035-declaration verified library with lemmas its own runs require, and records every run—accepted, downgraded, or failed—for future screening. Its headline artifact is a formalized estimator that attains the minimax rate 1/n + (d/(n log n))^2 for the average treatment effect under high-dimensional discrete confounding, closing a log-squared gap in the published upper bound.

Core claim

The paper's central claim is that proof soundness and statement faithfulness are two separate guarantees, and both are needed for an automated research system to produce trustworthy theorems. CausalForge pairs a Lean 4 kernel—which checks that a proof term types—with a statement-audit layer that compares each formal declaration against the natural-language claim stored on a logic-graph node, requiring logical equivalence in assumptions and conclusions. The flagship evidence is a formalized upper bound for the average treatment effect under high-dimensional discrete confounding: a hybrid plug-in/polynomial estimator attains rate 1/n + (d/(n log n))^2, matching the published lower bound and cl

What carries the argument

The logic graph: each result becomes a directed acyclic graph whose nodes are statements (setup, definition, assumption, lemma, theorem) carrying both a natural-language statement and a Lean 4 declaration, with edges separating what a statement means from what its proof uses. Nodes are labeled gated or cited; gated nodes sit on the critical path and must be proved, cited nodes are borrowed with source evidence. The statement-match gate re-audits each node and marks drift on any divergence, and the Lean 4 kernel checks every proof. This graph is what makes the two-part guarantee compositional and lets a changed statement reopen only its affected frontier.

Load-bearing premise

The load-bearing premise is that the LLM-based statement audit catches every mismatch between a formal Lean 4 statement and the intended natural-language claim; the paper reports no estimate of how often this audit errs.

What would settle it

A direct test would plant a known mismatch—say, a formal theorem with one extra hypothesis or a hardcoded constant—in an otherwise clean accepted-result graph and run the pipeline's statement audit on it; if the audit marks the planted node as matched rather than drift, the two-part guarantee fails. Measuring the audit's false-acceptance rate over a set of such planted mismatches would settle the question quantitatively.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • If CausalForge is right, a research pipeline can propose, formalize, prove, and write up causal-inference theorems while giving readers a per-node guarantee: the theorem compiles, and its formal statement was audited to match the intended claim.
  • The headline estimator, if accepted, settles the minimax MSE for ATE estimation under discrete confounding at rate n^{-1} + (d/(n log n))^2, with parametric order whenever d = O(sqrt(n log n)) and consistency exactly when d = o(n log n).
  • The library feedback channel implies that later runs become cheaper: lemmas proved for one result and promoted to the verified library are reused by later runs, and the paper documents concrete promotions such as an affinity bound for many hypotheses and a two-point reduction.
  • The run catalogue implies a sharp behavioral claim: the system's accepted self-proposed results are all technical gap-closers against published targets, while runs requiring a new identifying idea are downgraded for reducing to known constructions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the two-part guarantee is only as strong as the LLM statement audit; the paper explicitly declines to estimate its error rate, so the honest reading is that the guarantee is conditional on audit reliability rather than unconditional.
  • Editorial inference: the accepted-run asymmetry suggests a testable boundary for this whole class of systems: given a formal verifier, automated discovery will find technical gap-closers more readily than conceptual innovations, unless the proposal gate itself is improved; a matched-pair study within one cluster could confirm or refute this.
  • Editorial inference: the architecture's graph-and-audit machinery transfers to other fields, so the main cost of applying it elsewhere is building a comparable verified library rather than redesigning the agent loop.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents CausalForge, a framework for automated causal-inference research that couples a large Lean 4 formalization of causal inference (Causalean, 7,035 declarations) with an agentic discovery pipeline (CausalSmith). The pipeline proposes research questions, formalizes natural-language claims into Lean, constructs kernel-checked proofs, and uses a statement-audit layer to check that each formal statement matches the intended informal claim. The central advertised contribution is a two-part guarantee: proofs are machine-checked, and formal statements are the ones the paper reports. The evaluation reports 123 recorded runs, nine accepted results, and a flagship theorem that closes a log2-factor gap in the minimax ATE bound of Zeng et al. The paper is unusually candid about the limitations of its LLM-based statement audit and about the absence of independent significance evaluation.

Significance. If the two-part guarantee holds, the paper is a meaningful advance over both pure LLM-reviewed research agents and pure formal-verification pipelines: it adds a graph-localized, incremental statement-faithfulness audit to kernel-checked proof, and it demonstrates that this combination can produce at least one new theorem of independent interest (closing the Zeng et al. minimax gap). The self-improving library feedback loop is also of practical value. The paper ships the Lean library, pipeline code, and run records, which makes the proof-soundness component reproducible and externally checkable. The main open question concerns the reliability of the statement-audit layer, which the paper itself does not quantify.

major comments (3)
  1. [§1 and §7] The two-part guarantee advertised in §1 ('the proofs the pipeline produces are machine-checked, and the statements they establish are the ones the paper reports') depends on the statement audit of §5.3 being reliable. That audit is implemented with LLMs, and §7 explicitly states: 'a model can still err when auditing a statement, and we do not estimate how often it does.' No precision/recall measurement, human-labeled validation set, or adversarial injection study is reported. Since the audit is the only mechanism that catches the kernel-acceptable failures in Table 4 (wrong statements, vacuity, unproved shortcuts, over-narrow statements), an unmeasured error rate means the second half of the advertised guarantee is currently an unsupported assertion. This is a load-bearing gap, not a presentation issue, because the paper's distinctive contribution over prior formalization pipelines is pr
  2. [§6.3] The flagship result's formal proof is not independently verified in the manuscript; the claim rests on the Lean artifacts and on the paper's assertion that the twenty-six modules contain no forbidden tokens and that the headline theorem reduces to standard axioms. While this is a reasonable review model for a machine-checked development, the manuscript should provide more detailed evidence that the formal statement of the flagship theorem actually matches the informal claim (e.g., the exact statement of the theorem as checked against the graph node, or a human-verifiable statement-level excerpt). Without this, a reader cannot distinguish between 'the formal statement is the one described' and 'the formal statement was audited by the same class of system whose error rate is unknown.'
  3. [§6.2 and §6.5] The evaluation is small and self-reported: nine accepted results, with no baseline comparisons (e.g., a kernel-only pipeline without the statement audit, or an LLM-judge-only pipeline), no token/time cost accounting, and no independent significance panel. The paper is explicit about several of these limitations, and that candor is welcome. However, the central claim of the paper is about the statement audit's contribution, and the current evidence does not establish that the audit materially improves faithfulness over the kernel-only baseline, because no controlled comparison is reported. At minimum, an error-injection study on the audit — deliberately corrupting formal statements and measuring detection rates — would provide a direct test of the audit's reliability.
minor comments (4)
  1. [§8] Typo: 'provied from expert judgement' should be 'provided from expert judgment'.
  2. [Table 2 and §4.1] The declaration counts are reported as snapshot statistics and may change; the paper should make the snapshot date and commit hash of the library index explicit in the reproducibility section, not just the Lean toolchain pin.
  3. [§5.2] The sentence 'it may not weaken a statement merely to complete a proof or strengthen a hypothesis merely to obtain a result' is a strong constraint on the solver. It would be helpful to describe how this constraint is enforced mechanically (e.g., by diffing the solver's output against the typed core) versus by LLM judgment, since this is another place where the audit's reliability matters.
  4. [§6.3] The notation 'Rn,d,ϵ ≍ϵ ...' would be clearer if the dependence of the asymptotic constant on ϵ were stated explicitly, especially since the universal calibration is claimed not to take ϵ as input. A short remark on whether the constant is uniform in ϵ or only in n,d would improve readability.

Circularity Check

0 steps flagged

No circularity found: kernel-checked proofs rest on an external checker, and the LLM statement audit is an unvalidated reliability gap rather than a derivation that reduces to its inputs.

full rationale

The paper's derivation chain is not circular. Proof soundness is delegated to the Lean 4 kernel, an external, machine-checked benchmark, and the flagship result's lower bound is imported explicitly from external work rather than derived from the system's own outputs: 'the minimax lower half is not reproved here; it is transferred from the published moment-matching bound of Zeng et al. [54]... appears as an explicit hypothesis on the headline theorem—a cited node carrying its source—rather than an axiom inserted into the proof.' The statement-audit layer is performed by LLMs, and the paper candidly states its limitation: 'the faithfulness audit itself relies on an LLM... a model can still err when auditing a statement, and we do not estimate how often it does' (Section 7). This is a genuine unresolved reliability gap in the two-part guarantee's second pillar, but it is not circularity: the audit is an unvalidated component whose error rate is unmeasured, not a quantity defined in terms of the claim, fitted to the claim's conclusion, or justified by a self-citation chain. No fitted constants are presented as predictions; no uniqueness theorem from the authors' prior work is invoked to force a choice; and the only self-citation (Causalreasoningbenchmark, ref. [37]) appears in related work and is not load-bearing. The paper also explicitly reports that novelty tiers are LLM judgments and declines to treat them as validated evaluation, further separating its claims from its inputs. Accordingly, the correct circularity finding is no significant circularity; the audit-reliability concern belongs under correctness risk, not circularity.

Axiom & Free-Parameter Ledger

1 free parameters · 5 axioms · 0 invented entities

The proof-soundness guarantee rests on Lean/Mathlib and explicit handling of native decide artifacts. Mathematically, the flagship theorem imports the Zeng et al. lower bound as a hypothesis. The framework additionally assumes, without measurement, that LLM statement auditors are reliable enough to catch drift. No new physical or mathematical entities are postulated; the logic graph and review statuses are software artifacts.

free parameters (1)
  • Universal calibration constants in hybrid ATE estimator (split threshold, polynomial degree, variance normalization) = not stated
    Section 6.3 says a 'single universal numerical calibration' controls the heavy/light split, polynomial degree, and variance normalization, but no values are given. The rate theorem depends on the existence of such fixed constants.
axioms (5)
  • standard math Lean 4 kernel type theory and Mathlib are sound
    The framework's proof-soundness guarantee inherits trust in Lean; Section 3 explains that only the kernel decides whether a proof term has the claimed type.
  • standard math Native decide compiler artifacts are harmless and explicitly reported
    Section 4.5 reports that the only non-standard axioms are compiler artifacts from native decide; the paper asserts they are explicit and screened.
  • domain assumption The Zeng et al. minimax lower bound is correct and faithfully imported as a hypothesis
    Section 6.3 says the minimax lower half is not reproved and is transferred from [54] as an explicit hypothesis on the headline theorem. If that bound is wrong or mis-formalized, the headline claim fails.
  • domain assumption Strict-interior overlap, consistency, and conditional exchangeability define the ATE identification setting
    Section 6.3 states these as the conditions under which the flagship estimator attains the minimax rate; they are standard causal-inference assumptions and not proved in the paper.
  • ad hoc to paper LLM-based statement audit has sufficient reliability to catch statement drift
    Section 7 concedes 'the faithfulness audit itself relies on an LLM' and that 'a model can still err when auditing a statement, and we do not estimate how often it does.' The two-part guarantee depends on this unmeasured assumption.

pith-pipeline@v1.3.0-alltime-deepseek · 21797 in / 11858 out tokens · 112243 ms · 2026-08-01T04:30:24.754998+00:00 · methodology

0 comments
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2607.22511 by Jiyuan Tan, Vasilis Syrgkanis.

Figure 1
Figure 1. Figure 1: Causalean in layers: graphical and measure-theoretic foundations support the model languages, which support identification, which supports the estimation and design methods on top. A retrieval index over all 7,035 declarations spans the stack and is the interface the pipeline queries. 4.2 A tour of the clusters The library layers from graphical and measure-theoretic foundations up to the estimation and des… view at source ↗
Figure 2
Figure 2. Figure 2: The CausalSmith pipeline. Discovery includes topic selection: when a researcher does not supply a topic, a dedicated selector searches and ranks candidate directions, screens them against the run record, and admits a topic only after an adversarial quality gate. The resulting claim moves left to right through discovery, formalization, proof, and presentation, clearing a gate between stages (novelty and mat… view at source ↗
Figure 3
Figure 3. Figure 3: A logic graph (schematic). Nodes are statements; fill encodes review status ( [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Operational stage flow of a CausalSmith theorem run, with an inset zoom into the F2–F4 proof and statement-review loop. Top: Discovery (top band) produces a proposal and typed mathematical core, which is frozen at D0.5 and handed to Formalization (middle band). Gates (amber) may reject or return work to the preceding stage; four red diamonds mark run halts for external judgment: the D0-maximality checkpoin… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

56 extracted references · 33 linked inside Pith

  1. [1]

    CauSciBench: Can LLMs automate causal inference in real-world scientific research?arXiv preprint / OpenReview, 2025

    Sawal Acharya, Terry Jingchen Zhang, others, and Zhijing Jin. CauSciBench: Can LLMs automate causal inference in real-world scientific research?arXiv preprint / OpenReview, 2025. End-to-end causal-inference benchmark over real-world scientific research; causalNLP group

    2025

  2. [2]

    Faithful autoformalization via roundtrip verification and repair.arXiv preprint arXiv:2604.25031, 2026

    Daneshvar Amrollahi, Jerry Lopez, and Clark Barrett. Faithful autoformalization via roundtrip verification and repair.arXiv preprint arXiv:2604.25031, 2026

    Pith/arXiv arXiv 2026

  3. [3]

    Causal AI scientist: Towards end-to-end causal inference with large language models

    Anonymous. Causal AI scientist: Towards end-to-end causal inference with large language models. OpenReview submission (under review), 2026

    2026

  4. [4]

    Ayers, Dragomir Radev, and Jeremy Avigad

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics.arXiv preprint arXiv:2302.12433, 2023

    Pith/arXiv arXiv 2023

  5. [5]

    Evaluating Sakana’s AI scientist: Bold claims, mixed results, and a promising future?arXiv preprint arXiv:2502.14297, 2025

    Joeran Beel, Min-Yen Kan, and Moritz Baumgart. Evaluating Sakana’s AI scientist: Bold claims, mixed results, and a promising future?arXiv preprint arXiv:2502.14297, 2025

    arXiv 2025

  6. [6]

    Proof- Flow: A dependency graph approach to faithful proof autoformalization.arXiv preprint arXiv:2510.15981, 2025

    Rafael Cabral, Tuan Manh Do, Xuejun Yu, Wai Ming Tai, Zijin Feng, and Xin Shen. Proof- Flow: A dependency graph approach to faithful proof autoformalization.arXiv preprint arXiv:2510.15981, 2025

    arXiv 2025

  7. [7]

    Causal evaluation of language models.arXiv preprint arXiv:2405.00622, 2024

    Sirui Chen, Bo Peng, Meiqi Chen, Ruiqi Wang, Mengying Xu, Xingyu Zeng, Rui Zhao, Shengjie Zhao, Yu Qiao, and Chaochao Lu. Causal evaluation of language models.arXiv preprint arXiv:2405.00622, 2024. 18

    Pith/arXiv arXiv 2024

  8. [8]

    ORCA: ORchestrating causal agent

    Joanie Hayoun Chung, Sumin Lee, and Sungbin Lim. ORCA: ORchestrating causal agent. arXiv preprint arXiv:2508.21304, 2025. CHI EA 2026

    arXiv 2025

  9. [9]

    The signal-coverage matrix: Stratifying type and semantic errors in statement autoformalization.arXiv preprint arXiv:2606.28013, 2026

    Chengxiao Dai, Zhaokun Yan, and Zhanhui Lin. The signal-coverage matrix: Stratifying type and semantic errors in statement autoformalization.arXiv preprint arXiv:2606.28013, 2026

    Pith/arXiv arXiv 2026

  10. [10]

    The Lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. InAutomated Deduction (CADE 28), pages 625–635. Springer, 2021

    2021

  11. [11]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models.arXiv preprint arXiv:2303.04910, 2023

    Pith/arXiv arXiv 2023

  12. [12]

    Is ChatGPT a good causal reasoner? a comprehensive evaluation.Findings of the Association for Computational Linguistics: EMNLP,

    Jinglong Gao, Xiao Ding, Bing Qin, and Ting Liu. Is ChatGPT a good causal reasoner? a comprehensive evaluation.Findings of the Association for Computational Linguistics: EMNLP,

  13. [13]

    EconCSLib: AI-assisted lean formalization for economics and computation research.arXiv preprint arXiv:2606.13306, 2026

    Nikhil Garg. EconCSLib: AI-assisted lean formalization for economics and computation research.arXiv preprint arXiv:2606.13306, 2026

    Pith/arXiv arXiv 2026

  14. [14]

    Towards an AI co-scientist.arXiv preprint arXiv:2502.18864, 2025

    Juraj Gottweis, Wei-Hung Weng, Alexander Daryin, Tao Tu, Anil Palepu, Vivek Natarajan, et al. Towards an AI co-scientist.arXiv preprint arXiv:2502.18864, 2025

    Pith/arXiv arXiv 2025

  15. [15]

    Mining causality: AI-assisted search for instrumental variables.arXiv preprint arXiv:2409.14202, 2024

    Sukjin Han. Mining causality: AI-assisted search for instrumental variables.arXiv preprint arXiv:2409.14202, 2024

    Pith/arXiv arXiv 2024

  16. [16]

    Olympiad-level formal mathematical reasoning with reinforcement learning.Nature, 2025

    Thomas Hubert, Rishi Mehta, Laurent Sartran, et al. Olympiad-level formal mathematical reasoning with reinforcement learning.Nature, 2025. DOI: 10.1038/s41586-025-09833-y

    doi:10.1038/s41586-025-09833-y 2025

  17. [17]

    Sorries are not the hard part: An expert-review case study of a semi-autonomous formalization.arXiv preprint arXiv:2606.13925, 2026

    Vasily Ilin and Brian Nugent. Sorries are not the hard part: An expert-review case study of a semi-autonomous formalization.arXiv preprint arXiv:2606.13925, 2026

    arXiv 2026

  18. [18]

    Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timoth´ ee Lacroix, Yuhuai Wu, and Guillaume Lample

    Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timoth´ ee Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. InInternational Conference on Learning Representations (ICLR), 2023

    2023

  19. [19]

    BadScientist: Can a research agent write convincing but unsound papers that fool LLM reviewers?arXiv preprint arXiv:2510.18003, 2025

    Fengqing Jiang, Yichen Feng, Yuetai Li, Luyao Niu, Basel Alomair, and Radha Poovendran. BadScientist: Can a research agent write convincing but unsound papers that fool LLM reviewers?arXiv preprint arXiv:2510.18003, 2025

    Pith/arXiv arXiv 2025

  20. [20]

    CLadder: Assessing causal reasoning in language models

    Zhijing Jin, Yuen Chen, Felix Leeb, Luigi Gresele, Ojasv Kamal, Zhiheng Lyu, Kevin Blin, Fernando Gonzalez Adauto, Max Kleiman-Weiner, Mrinmaya Sachan, and Bernhard Sch¨ olkopf. CLadder: Assessing causal reasoning in language models. InAdvances in Neural Information Processing Systems (NeurIPS), 2023

    2023

  21. [21]

    Can large language models infer causation from correlation? In International Conference on Learning Representations (ICLR), 2024

    Zhijing Jin, Jiarui Liu, Zhiheng Lyu, Spencer Poff, Mrinmaya Sachan, Rada Mihalcea, Mona Diab, and Bernhard Sch¨ olkopf. Can large language models infer causation from correlation? In International Conference on Learning Representations (ICLR), 2024

    2024

  22. [22]

    LLMs are prone to fallacies in causal inference.arXiv preprint arXiv:2406.12158, 2024

    Nitish Joshi, Abulhair Saparov, Yixin Wang, and He He. LLMs are prone to fallacies in causal inference.arXiv preprint arXiv:2406.12158, 2024. 19

    Pith/arXiv arXiv 2024

  23. [23]

    Causal reasoning and large language models: Opening a new frontier for causality.Transactions on Machine Learning Research, 2023

    Emre Kıcıman, Robert Ness, Amit Sharma, and Chenhao Tan. Causal reasoning and large language models: Opening a new frontier for causality.Transactions on Machine Learning Research, 2023. arXiv:2305.00050

    Pith/arXiv arXiv 2023

  24. [24]

    HyperTree proof search for neural theorem proving.arXiv preprint arXiv:2205.11491, 2022

    Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurelien Rodriguez, and Timothee Lacroix. HyperTree proof search for neural theorem proving.arXiv preprint arXiv:2205.11491, 2022

    Pith/arXiv arXiv 2022

  25. [25]

    Formalization of optimality conditions for smooth constrained optimization problems.arXiv preprint arXiv:2503.18821, 2025.https://github.com/optsuite/optlib

    Chenyi Li, Shengyang Xu, Chumin Sun, Li Zhou, and Zaiwen Wen. Formalization of optimality conditions for smooth constrained optimization problems.arXiv preprint arXiv:2503.18821, 2025.https://github.com/optsuite/optlib

    Pith/arXiv arXiv 2025

  26. [26]

    Autoformalize mathematical statements by symbolic equivalence and semantic consistency

    Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In Advances in Neural Information Processing Systems (NeurIPS), 2024. arXiv:2410.20936

    Pith/arXiv arXiv 2024

  27. [27]

    Are LLMs capable of data-based statistical and causal reasoning? benchmarking advanced quantitative reasoning with data

    Xiao Liu, Zirui Wu, Xueqing Wu, Pan Lu, Kai-Wei Chang, and Yansong Feng. Are LLMs capable of data-based statistical and causal reasoning? benchmarking advanced quantitative reasoning with data. InFindings of the Association for Computational Linguistics: ACL, 2024. arXiv:2402.17644

    Pith/arXiv arXiv 2024

  28. [28]

    For- malAlign: Automated alignment evaluation for autoformalization

    Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, and Zhijiang Guo. For- malAlign: Automated alignment evaluation for autoformalization. InInternational Conference on Learning Representations (ICLR), 2025. arXiv:2410.10135

    Pith/arXiv arXiv 2025

  29. [29]

    Causal inference with large language model: A survey

    Jing Ma. Causal inference with large language model: A survey. InFindings of the Association for Computational Linguistics: NAACL 2025, pages 5901–5913. Association for Computational Linguistics, 2025. doi: 10.18653/v1/2025.findings-naacl.327. URL https://aclanthology. org/2025.findings-naacl.327/

    doi:10.18653/v1/2025.findings-naacl.327 2025

  30. [30]

    Formalizing numerical analysis: An agent pipeline and quality audit beyond kernel acceptance.arXiv preprint arXiv:2606.14000, 2026

    Theodore Meek, Siyuan Ge, Di Qiu Xiang, Simon Chess, and Vasily Ilin. Formalizing numerical analysis: An agent pipeline and quality audit beyond kernel acceptance.arXiv preprint arXiv:2606.14000, 2026. Verify author-name segmentation against the arXiv page

    arXiv 2026

  31. [31]

    Mohammad and Tamim Sheikh

    Noor Islam S. Mohammad and Tamim Sheikh. The faithfulness gap: Certifying semantic equivalence between natural-language and formal mathematical statements.arXiv preprint arXiv:2606.16541, 2026

    arXiv 2026

  32. [32]

    Alexander Novikov, Ngˆ an V˜ u, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. AlphaEvolve: A coding agent for scientific and al...

    Pith/arXiv arXiv 2025

  33. [33]

    Reliable evaluation and benchmarks for statement autoformalization.Findings of the Association for Computational Linguistics: EMNLP, 2025

    Auguste Poiroux, Gail Weiss, Viktor Kunˇ cak, and Antoine Bosselut. Reliable evaluation and benchmarks for statement autoformalization.Findings of the Association for Computational Linguistics: EMNLP, 2025. arXiv:2406.07222

    arXiv 2025

  34. [34]

    Generative language modeling for automated theorem proving.arXiv preprint arXiv:2009.03393, 2020

    Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving.arXiv preprint arXiv:2009.03393, 2020. 20

    Pith/arXiv arXiv 2009

  35. [35]

    Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition.arXiv preprint arXiv...

    Pith/arXiv arXiv 2025

  36. [36]

    Pawan Kumar, Emilien Dupont, Francisco J

    Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. Mathematical discoveries from program search with large language models.Nature, 625:468–475, 2024

    2024

  37. [37]

    Causalreasoningbenchmark: A real-world benchmark for disentangled evaluation of causal identification and estimation, 2026

    Ayush Sawarni, Jiyuan Tan, and Vasilis Syrgkanis. Causalreasoningbenchmark: A real-world benchmark for disentangled evaluation of causal identification and estimation, 2026

    2026

  38. [38]

    Exploring multi-modal data with tool-augmented LLM agents for precise causal discovery

    ChengAo Shen, Zhengzhang Chen, Dongsheng Luo, Dongkuan Xu, Haifeng Chen, and Jingchao Ni. Exploring multi-modal data with tool-augmented LLM agents for precise causal discovery. arXiv preprint arXiv:2412.13667, 2024

    Pith/arXiv arXiv 2024

  39. [39]

    IV co-scientist: Multi-agent LLM framework for causal instrumental variable discovery.arXiv preprint arXiv:2602.07943, 2026

    Ivaxi Sheth, Zhijing Jin, Bryan Wilder, Dominik Janzing, and Mario Fritz. IV co-scientist: Multi-agent LLM framework for causal instrumental variable discovery.arXiv preprint arXiv:2602.07943, 2026

    Pith/arXiv arXiv 2026

  40. [40]

    Lean copilot: Large language models as copilots for theorem proving in lean.arXiv preprint arXiv:2404.12534, 2024

    Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Lean copilot: Large language models as copilots for theorem proving in lean.arXiv preprint arXiv:2404.12534, 2024

    Pith/arXiv arXiv 2024

  41. [41]

    Lean formal- ization of generalization error bound by Rademacher complexity and Dudley’s entropy integral

    Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, and Naoto Onda. Lean formal- ization of generalization error bound by Rademacher complexity and Dudley’s entropy integral. arXiv preprint arXiv:2503.19605, 2025.https://github.com/auto-res/lean-rademacher

    Pith/arXiv arXiv 2025

  42. [42]

    The Lean mathematical library

    The mathlib Community. The Lean mathematical library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pages 367–381, 2020

    2020

  43. [43]

    Trinh, Yuhuai Wu, Quoc V

    Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations.Nature, 625:476–482, 2024. doi: 10.1038/s41586-023-06747-5

    doi:10.1038/s41586-023-06747-5 2024

  44. [44]

    PutnamBench: Evaluating neural theorem-provers on the Putnam mathematical competition.Advances in Neural Information Processing Systems (NeurIPS), 2024

    George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. PutnamBench: Evaluating neural theorem-provers on the Putnam mathematical competition.Advances in Neural Information Processing Systems (NeurIPS), 2024. arXiv:2407.11214

    Pith/arXiv arXiv 2024

  45. [45]

    Ulu¸ san, Burak S

    Zeynel A. Ulu¸ san, Burak S. Akbudak, Can S. Erer, and G¨ ozde G¨ ulS ¸ahin. FormalRewardBench: A benchmark for formal theorem proving reward models.arXiv preprint arXiv:2605.10141, 2026

    Pith/arXiv arXiv 2026

  46. [46]

    Causal-Copilot: An autonomous causal analysis agent.arXiv preprint arXiv:2504.13263, 2025

    Xinyue Wang, Kun Zhou, Wenyi Wu, Har Simrat Singh, Fang Nan, Songyao Jin, Aryan Philip, Saloni Patnaik, Hou Zhu, Shivam Singh, Parjanya Prashant, Qian Shen, and Biwei Huang. Causal-Copilot: An autonomous causal analysis agent.arXiv preprint arXiv:2504.13263, 2025

    Pith/arXiv arXiv 2025

  47. [47]

    Fang, and Junwei Lu

    Tingzhou Wei, Zeyu Zheng, Ethan X. Fang, and Junwei Lu. Hypothesis-disciplined multi-agent automated formalization of asymptotic statistical theory.arXiv preprint arXiv:2606.20642, 2026. 21

    Pith/arXiv arXiv 2026

  48. [48]

    Jiang, Wenda Li, Markus N

    Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. InAdvances in Neural Information Processing Systems (NeurIPS), 2022

    2022

  49. [49]

    The AI scientist-v2: Workshop-level automated scientific discovery via agentic tree search.arXiv preprint arXiv:2504.08066, 2025

    Yutaro Yamada, Robert Tjarko Lange, Cong Lu, Shengran Hu, Chris Lu, Jakob Foerster, Jeff Clune, and David Ha. The AI scientist-v2: Workshop-level automated scientific discovery via agentic tree search.arXiv preprint arXiv:2504.08066, 2025

    Pith/arXiv arXiv 2025

  50. [50]

    Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

    Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval- augmented language models. InAdvances in Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track, 2023

    2023

  51. [51]

    Formal mathematical reasoning: A new frontier in AI.arXiv preprint arXiv:2412.16075, 2024

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in AI.arXiv preprint arXiv:2412.16075, 2024

    Pith/arXiv arXiv 2024

  52. [52]

    A critical review of causal reasoning benchmarks for large language models.arXiv preprint arXiv:2407.08029, 2024

    Linying Yang, Vik Shirvaikar, Oscar Clivio, and Fabian Falck. A critical review of causal reasoning benchmarks for large language models.arXiv preprint arXiv:2407.08029, 2024

    Pith/arXiv arXiv 2024

  53. [53]

    Causal parrots: Large language models may talk causality but are not causal.Transactions on Machine Learning Research, 2023

    Matej Zeˇ cevi´ c, Moritz Willig, Devendra Singh Dhami, and Kristian Kersting. Causal parrots: Large language models may talk causality but are not causal.Transactions on Machine Learning Research, 2023. arXiv:2308.13067

    Pith/arXiv arXiv 2023

  54. [54]

    Zhenghao Zeng, Sivaraman Balakrishnan, Yanjun Han, and Edward H. Kennedy. Causal inference with high-dimensional discrete covariates.arXiv preprint arXiv:2405.00118, 2024

    Pith/arXiv arXiv 2024

  55. [55]

    MiniF2F: A cross-system benchmark for formal olympiad-level mathematics.arXiv preprint arXiv:2109.00110, 2021

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: A cross-system benchmark for formal olympiad-level mathematics.arXiv preprint arXiv:2109.00110, 2021

    Pith/arXiv arXiv 2021

  56. [56]

    LeanArchitect: Automating blueprint generation for humans and AI.arXiv preprint arXiv:2601.22554, 2026

    Thomas Zhu, Pietro Monticone, Jeremy Avigad, and Sean Welleck. LeanArchitect: Automating blueprint generation for humans and AI.arXiv preprint arXiv:2601.22554, 2026. A Flagship theorem locations For reproducibility, Table 7 gives theLean 4declaration name and source location of each flagship result named in Section 4.3. All locations are relative to the ...

    arXiv 2026