Pith. sign in

REVIEW 4 major objections 6 minor 2 cited by

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

T0 review · 4 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read A two-model pipeline—one model proposing lemma statements, another verifying them—produces machine-verified Lean proofs for five post-2000 IMO problems.

desk verdict Five Lean proofs and a clean decoupling story, but the missing direct-proving control and unreported attempt pool keep the central claim from being fully established. read the letter →

arxiv 2507.06804 v1 pith:PZBEA2OB submitted 2025-07-07 cs.LO cs.AI

Zhenwen Liang , Linfeng Song , Yang Li , Tao Yang , Feng Zhang , Haitao Mi , Dong Yu This is my paper · ORCID
classification cs.LOcs.AI MSC 03B3568V05
keywords automatedtheoremprovingLeanformalproofsIMOproblemsdecoupledreasoningandsubgoallemmaslargelanguagemodelsreinforcementlearningwithverifiablerewardsreasoning-provinggap
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Large language models can reason about hard mathematics informally—over 80% accuracy on PutnamBench—but their formally verified proofs lag far behind, below 8%. This paper argues that the gap is self-inflicted: state-of-the-art provers couple planning and proof generation inside one model trained to maximize the binary reward of a completed proof, which pushes them toward shallow tactic-bashing instead of deep strategy. The proposed fix is a decoupled pipeline in which a general-purpose Reasoner emits only formal lemma statements, a specialized Prover checks each lemma, and a final model assembles the proof from the verified lemmas. On a set of post-2000 non-geometry IMO problems where the authors state no open-source prover had previously reported a success, the pipeline produces machine-verified Lean proofs for five: IMO 2000 P2, 2005 P3, 2011 P3, 2019 P1, and 2020 P2. A sympathetic reader should take the paper as evidence that the bottleneck in formal proving is not raw reasoning power but the architecture that couples reasoning to tactic-level proof search.

What carries the argument

The load-bearing mechanism is the subgoal-lemma bridge. The Reasoner (the authors use Gemini 2.5 Pro) is prompted to think through a proof strategy and output only the formal Lean statements of intermediate theorems, terminated by 'by sorry'; a regular expression extracts the declarations. The Prover (DeepSeek-Prover-v2 7B, CoT variant) then attempts each lemma with up to $k=128$ proof candidates, retaining only lemmas for which at least one attempt succeeds. Finally, a model adept at proof continuation (OpenAI-o3 or Gemini 2.5 Pro) receives the verified lemmas in context and assembles the main proof. The framework also documents a phenomenon the authors call 'contextual blindness': many provers ignore pre-proven standalone lemmas and try to reprove the theorem from scratch, which is why the final stage uses reasoner models rather than the specialized prover.

What would settle it

Publishing the complete list of attempted post-2000 IMO problems with per-problem outcomes, or re-running the pipeline with open-weights models and fully specified prompts, would settle the claim. Concretely: if the attempted set is shown to include many more than the five reported problems, or if an independent run with the same prompts on the stated API models fails to reproduce even one of the five verified proofs, the central claim would be refuted.

Watch

Extended reading notes

Core claim

The paper's central claim is that high-level mathematical reasoning and low-level formal proof generation should be performed by distinct, specialized models: a Reasoner that proposes strategic subgoal lemmas as formal statements, and a Prover that verifies them. The authors identify the prevailing training paradigm—reinforcement learning with verifiable rewards, which rewards only final proof success—as the root cause of the reasoning-proving gap, arguing that it degrades the latent reasoning of prover models and encourages brute-force tactic application. As evidence, they report that a specialized prover (Kimina-Prover) scores lower than its general-purpose base model (Qwen2.5-Math-7B-Instruct) on MATH and AIME24, and they present a case study on IMO 2019 P1 in which a monolithic prover's attempts reduce to flat instantiations and tactic calls, while the decoupled Reasoner recovers the shifted-Cauchy structure of the solution. The paper's headline result is that the decoupled framework produces verified Lean proofs for five post-2000 IMO problems that, on the paper's problem set, no prior open-source prover had solved.

Load-bearing premise

The whole result rests on the unstated size of the attempted IMO problem set and on the closed API models used for the final proof assembly: if the five solved problems were selected from a much larger pool, or if the commercial reasoners needed human-tuned prompts or oracle hints, the claim of first success on this problem set loses its force.

Editorial extensions

If this is right

  • If the decoupling principle is correct, the poor formal-proving performance of LLMs is not a reasoning deficit but a training and architecture artifact, so the same general-purpose reasoning models that score high on informal benchmarks can be redirected into formal proof search.
  • The five verified Lean proofs become concrete baselines: any future open-source prover can be checked against them, and the released verified-lemma dataset gives the community intermediate milestones for problems that remain unsolved.
  • The pipeline's bottleneck analysis implies that improving the Prover—either by stronger proof search or by fine-tuning provers to use given lemmas—should directly increase the number of solvable IMO problems, since an oracle experiment with human-proved lemmas solved significantly more.
  • The RLVR degradation result suggests that training signals for provers should reward strategic structure or lemma use, not only final proof success, if the community wants provers that scale to olympiad-level problems.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper never states how many post-2000 non-geometry IMO problems were attempted, so the five successes cannot yet be converted into a success rate; if the intended denominator is roughly the one hundred non-geometry problems from 2000 to 2024, the correct headline would be 'five of about one hundred,' not simply 'five solved.'
  • If the diagnosis generalizes, the same decoupled design should transfer to other proof assistants and to non-competition mathematics: any domain where a strong informal reasoner can name the right intermediate statements while a weaker tactic engine verifies them.
  • A testable extension would be to run the full pipeline with an open-weights Reasoner and fully public prompts; if the same five problems still verify, the result would no longer depend on closed API models.
  • The Kimina/Qwen degradation comparison is a single model pair, so the claimed RLVR-induced degeneration would be stronger if replicated across other prover/base-model pairs.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

Summary. The paper proposes DRP-IMO, a three-stage pipeline for Lean 4 theorem proving in which a general-purpose LLM Reasoner generates formal subgoal lemma statements, an open-source Prover (DeepSeek-Prover-v2, 7B CoT) attempts to verify those lemmas, and a final assembly stage uses OpenAI-o3 or Gemini 2.5 Pro to combine the verified lemmas into a proof of the main IMO problem. The authors report success on five post-2000 non-geometry IMO problems: IMO 2000 P2, IMO 2005 P3, IMO 2011 P3, IMO 2019 P1, and IMO 2020 P2. They also present a qualitative case study on IMO 2019 P1, a small quantitative experiment on reasoning degradation in Kimina-Prover, an oracle experiment suggesting that the Prover is the main bottleneck, and a release of verified lemmas for a broader set of IMO problems. The central claim is that decoupling reasoning from proving enables machine-verified solutions on problems where prior open-source provers have reported no success.

Significance. If the five proofs are correct and the attribution to the decoupled architecture is valid, this is a meaningful advance: it would provide the first open-source-adjacent pipeline that machine-verifies several difficult post-2000 IMO problems, and the released lemma dataset could be a useful resource. The paper also makes a falsifiable architectural claim about the benefit of separating strategic reasoning from tactical proof search. However, the significance is conditional on reproducibility and on controls that the current manuscript does not provide; the final proofs are generated by closed commercial models, and no direct-proving baseline is reported for those models.

major comments (4)
  1. [Section 3.3 and Appendix B] The final proofs of all five solved problems are produced by OpenAI-o3 or Gemini 2.5 Pro, not by the open-source Prover (DeepSeek-Prover-v2) that is the named Prover component in the paper's framing. The manuscript reports that DeepSeek-Prover-v2 ignores provided lemmas, but it does not report any direct-proving baseline in which OpenAI-o3 or Gemini 2.5 Pro attempt the same five Lean statements without the decoupled subgoal pipeline and with the same compute budget (k=128). Without this ablation, the observed successes cannot be attributed to the decoupled architecture; they may reflect the raw proving capability of the closed models. This is the load-bearing control for the paper's central claim and must be added.
  2. [Section 4] The evaluation reports only the five successes and never states the total number of non-geometry post-2000 IMO problems that were attempted, nor a per-problem breakdown of lemma-generation and verification outcomes. The abstract's phrase 'solves 5 of these problems' is therefore compatible with a much larger attempted set, and the claim that this problem set is one 'on which no prior open-source prover has reported success' is likewise asserted without a citation or a systematic comparison. The paper should report the full attempted set, the success/failure status of every problem, and the basis for the no-prior-success claim.
  3. [Sections 3.2, 3.3, and Appendix B] The paper's main evidence consists of five Lean proof scripts, but no build environment, Mathlib version, Lean toolchain version, commit hash, or exact inference prompts and hyperparameters are provided. Several proof scripts use very heavy tactic combinations (e.g., `maxHeartbeats 0`, repeated `nlinarith`, `ring_nf`, `aesop`, `omega`) and contain notation that is not obviously standard Lean 4; as a referee I cannot determine from the text alone whether the Appendix B files compile as printed. The authors should ship a reproducible artifact with exact versions and commands, and confirm that each listed proof compiles in that environment.
  4. [Section 4.1 and Section 4.2] The qualitative comparison in Section 4.1 is based on three sampled, partially quoted attempts from DeepSeek-Prover-v2 and is not a controlled experiment; it cannot support the claim that the decoupled framework's reasoning path is the cause of success. Similarly, the RLVR-degradation experiment in Section 4.2 uses one base model and one prover derived from it, with no error bars or repetition across models; the reported drops, especially at pass@1, are suggestive but not strong enough to carry the paper's motivational thesis. These sections should be reframed as illustrative or supplemented with a systematic comparison on the solved problem set.
minor comments (6)
  1. [Section 4] There are typographical errors such as 'experiemnts' in Section 4; the paper should be copy-edited.
  2. [Section 3.3] The text describing the final proof construction appears twice with slightly different wording; one of the duplicated paragraphs should be removed.
  3. [Figure 1] Figure 1 is difficult to read at the resolution provided; the subgoal statements and the correspondence between reasoning steps and formal lemmas should be presented more legibly.
  4. [Table 1] Table 1 reports pass@k only for AIME24 and only pass@1 for MATH; the sampling setup, the number of samples, and whether pass@k is unbiased are not specified, so the numerical comparisons should be interpreted cautiously.
  5. [Abstract and Section 1] The paper refers to PutnamBench and to the claim that informal accuracy exceeds 80% while formal success is below 8%, but the precise source of these numbers should be cited directly rather than cited only through a general reference.
  6. [Appendix B] The theorem names are inconsistent across the appendix (e.g., `imo2019_p1` in some places and `imo2020_q2` in others); uniform naming would improve readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the five claimed IMO solutions are checked by Lean's kernel, the subgoal lemmas are proved before final assembly, and no fitted parameter is renamed as a prediction.

full rationale

After walking the derivation chain, I find no step in which a predicted quantity is definitionally equal to an input, a fitted parameter is renamed as a prediction, or a load-bearing premise is imported solely from the authors' own prior work. The five claimed successes are grounded in Lean code checked against an external kernel; the intermediate lemmas in Appendix B are stated as separate theorems and proved before final assembly. The final proofs (e.g., B.2 for IMO 2019 P1) invoke only the previously proved subgoal lemmas and basic tactics, so the final theorem is not the same object as any single subgoal by construction. The motivating claim that RLVR degrades reasoning (Section 4.2, Table 1) is an empirical comparison between a base model and a fine-tuned prover; it is used to justify the architecture, but the architecture's successes are not defined in terms of that comparison, so the motivation is not circular. The paper's self-citations (HunyuanProver, MPS-Prover) appear only in related work and are not load-bearing. The main weaknesses—the unreported denominator of attempted problems, closed API models performing final assembly, and the absence of a direct-proving baseline for those models—are attribution and reproducibility concerns, not circularity. No specific reduction of a result to its inputs can be quoted; therefore the circularity score is 0.

Assumptions & free parameters 1 free parameters · 2 assumptions · 0 invented entities

No fitted constants appear in the proofs themselves; the only free parameter is the number of proof candidates k=128. The framework introduces no new mathematical entities. The main assumptions are the soundness of the Lean checker and the availability of the closed API models used for final proof assembly.

free parameters (1)
  • number of proof candidates k = 128
    Section 3.2 sets k=128, described as 'chosen empirically to balance exploration breadth against computational cost.' This affects which lemmas are retained as verified and therefore the final outcome.
assumptions (2)
  • domain assumption Lean 4 kernel and Mathlib are sound and the appended proofs compile
    The central result is the machine-checked formal proofs; the paper does not provide build artifacts, commit hashes, or instructions to recompile, so this is assumed from the paper's claim.
  • domain assumption The arithmetic tactics used (nlinarith, omega, ring_nf) solve the stated goals exactly
    These tactics are trusted black boxes in the appended proofs; their correctness is assumed.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving." pith.science (2026). https://pith.science/paper/PZBEA2OB

@misc{pith2026250706804,
  author       = {Pith},
  title        = {Pith review of: Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PZBEA2OB}},
  note         = {Machine review of arXiv:2507.06804}
}
read the original abstract

Automated Theorem Proving (ATP) in formal languages is a foundational challenge for AI. While Large Language Models (LLMs) have driven remarkable progress, a significant gap remains between their powerful informal reasoning capabilities and their weak formal proving performance. Recent studies show that the informal accuracy exceeds 80% while formal success remains below 8% on benchmarks like PutnamBench. We argue this gap persists because current state-of-the-art provers, by tightly coupling reasoning and proving, are trained with paradigms that inadvertently punish deep reasoning in favor of shallow, tactic-based strategies. To bridge this fundamental gap, we propose a novel framework that decouples high-level reasoning from low-level proof generation. Our approach utilizes two distinct, specialized models: a powerful, general-purpose Reasoner to generate diverse, strategic subgoal lemmas, and an efficient Prover to rigorously verify them. This modular design liberates the model's full reasoning potential and bypasses the pitfalls of end-to-end training. We evaluate our method on a challenging set of post-2000 IMO problems, a problem set on which no prior open-source prover has reported success. Our decoupled framework successfully solves 5 of these problems, demonstrating a significant step towards automated reasoning on exceptionally difficult mathematical challenges. To foster future research, we release our full dataset of generated and verified lemmas for a wide range of IMO problems, available at https://tencent-imo.github.io/ .

Figures

Figures reproduced from arXiv: 2507.06804 by the authors.

Figure 1
Figure 1. The overall pipeline of DRP-IMO taking the problem of IMO 2019 P1 as an example. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Kimina solutions to amc12b_2002_p7. The have statements [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    cs.CL 2026-07 accept novelty 6.0 of 10

    LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.

  2. Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

    cs.CL 2025-07 conditional novelty 6.0 of 10

    A minimal-prior pipeline with automated data curation and verifier-driven RL lets small LLMs generate verifiable Dafny specifications and beat larger proprietary models on a synthetic compositional benchmark.

Reference graph

Works this paper leans on

22 extracted references · 6 canonical work pages · cited by 2 Pith papers

  1. [1]

    Reviving dsp for advanced theorem proving in the era of reasoning models

    Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. Reviving dsp for advanced theorem proving in the era of reasoning models. arXiv preprint arXiv:2506.11487, 2025

    arXiv 2025

  2. [2]

    The open proof corpus: A large-scale study of llm-generated mathematical proofs

    Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Mislav Balunovic, Martin Vechev, Miroslav Marinov, Maria Drencheva, Lyuba Konova, Milen Shumanov, Kaloyan Tsvetkov, et al. The open proof corpus: A large-scale study of llm-generated mathematical proofs. arXiv preprint arXiv:2506.21621, 2025

    arXiv 2025

  3. [3]

    Baldur: Whole-proof generation and repair with large language models

    Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp.\ 1229--1241, 2023

    work page 2023

  4. [4]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023. URL https://openreview.net/forum?id=SMa9EAovKMC

    2023

  5. [5]

    Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving

    Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024

    arXiv 2024

  6. [6]

    Mps-prover: Advancing stepwise theorem proving by multi-perspective search and data curation

    Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, and Dong Yu. Mps-prover: Advancing stepwise theorem proving by multi-perspective search and data curation. arXiv preprint arXiv:2505.10962, 2025

    arXiv 2025

  7. [7]

    Goedel-prover: A frontier model for open-source automated theorem proving

    Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025

    arXiv 2025

  8. [8]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction--CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12--15, 2021, Proceedings 28, pp.\ 625--635. Springer, 2021

    work page 2021

Show all 22 references
  1. [9]

    Isabelle: A generic theorem prover

    Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994

    1994

  2. [10]

    Generative language modeling for automated theorem proving

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

    2009 arXiv

  3. [11]

    Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition

    ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025

    2025 arXiv

  4. [12]

    Proving theorems recursively

    Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng YANG, Jing Tang, Jian Yin, Zhenguo Li, and Xiaodan Liang. Proving theorems recursively. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024 a . URL https://...

    2024

  5. [13]

    LEGO -prover: Neural theorem proving with growing libraries

    Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. LEGO -prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Repres...

    2024

  6. [15]

    Internlm2.5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems

    Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2.5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024

  7. [16]

    Deepseek-prover-v1

    Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024

    2024 arXiv

  8. [17]

    Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving

    Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025

    2025

  9. [18]

    Subgoalxl: Subgoal-based expert learning for theorem proving

    Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker, and Lingpeng Kong. Subgoalxl: Subgoal-based expert learning for theorem proving. arXiv preprint arXiv:2408.11172, 2024

    2024 arXiv

  10. [19]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

  11. [20]

    @esa (Ref

    \@ifxundefined[1] #1\@undefined \@firstoftwo \@secondoftwo \@ifnum[1] #1 \@firstoftwo \@secondoftwo \@ifx[1] #1 \@firstoftwo \@secondoftwo [2] @ #1 \@temptokena #2 #1 @ \@temptokena \@ifclassloaded agu2001 natbib The agu2001 class already includes natbib coding, so you should ...

  12. [21]

    \@lbibitem[] @bibitem@first@sw\@secondoftwo \@lbibitem[#1]#2 \@extra@b@citeb \@ifundefined br@#2\@extra@b@citeb \@namedef br@#2 \@nameuse br@#2\@extra@b@citeb \@ifundefined b@#2\@extra@b@citeb @num @parse #2 @tmp #1 NAT@b@open@#2 NAT@b@shut@#2 \@ifnum @merge>\@ne @bibitem@firs...

  13. [22]

    v+*f = Y) ӈ/F=< !Ǔo N1㚘S!f q9 *(mO m #0`

    @open @close @open @close and [1] URL: #1 \@ifundefined chapter * \@mkboth \@ifxundefined @sectionbib * \@mkboth * \@mkboth\@gobbletwo \@ifclassloaded amsart * \@ifclassloaded amsbook * \@ifxundefined @heading @heading NAT@ctr thebibliography [1] @ \@biblabel @NAT@ctr \@bibset...

    2022

  14. [23]

    @open @close @open @close and [1] URL: #1 \@ifundefined chapter * \@mkboth \@ifxundefined @sectionbib * \@mkboth * \@mkboth\@gobbletwo \@ifclassloaded amsart * \@ifclassloaded amsbook * \@ifxundefined @heading @heading NAT@ctr thebibliography [1] @ \@biblabel @NAT@ctr \@bibset...

    2020 arXiv

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.