Pith. sign in

REVIEW 2 major objections 6 minor 1 cited by

A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems

T0 review · 2 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read The paper provides public Lean proofs for 17 IMO problems that lacked them, decomposes 13 of those proofs into 1,329 machine-checked lemmas, and reports that state-of-the-art LLMs prove at most 39.3% of those lemmas.

desk verdict A valuable, machine-checked dataset of IMO proofs and lemmas, but the headline LLM accuracies mix two task types the paper never separates. read the letter →

arxiv 2411.18872 v2 pith:DQST3VNV submitted 2024-11-28 cs.LG

Roozbeh Yousefzadeh , Xuenan Cao , Azim Ospanov This is my paper · ORCID
classification cs.LG
keywords LeanformalproofinteractivetheoremprovingInternationalMathOlympiadminiF2FlemmadecompositionLLMevaluationautomated
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

This paper tries to remove a basic obstacle for AI systems that prove hard mathematics: for almost half of the IMO problems in the standard miniF2F benchmark, no correct formal proof was publicly available, so failures could not be diagnosed. The authors write complete Lean proofs for the 14 missing miniF2F IMO problems plus three from IMO 2022 and 2023, then break 13 of those proofs into 1,329 smaller verified lemmas that form a stepping-stone dataset. They evaluate several state-of-the-art LLMs on these lemmas and report that the best model, DeepSeek-Prover-V1.5-RL, proves only 39.3% of them, while o3-mini reaches 23.8% after ten rounds of automated feedback and general-purpose math models prove 1 or 0 lemmas. If these lemmas really are the building blocks of IMO proofs, the dataset lets the community locate exactly where automated provers break down and measure progress well before full olympiad problems are solved.

What carries the argument

The central object is a proof-decomposition procedure that turns one long formal proof into a dataset of approachable building-block lemmas. The procedure finds intermediate hypotheses inside a proof, states each hypothesis as a standalone lemma, and also creates new lemmas by granting some of those hypotheses back to the original statement so that each extracted lemma has a proof that is a segment of the full proof. Lean's type checker is the machine that certifies every lemma, and lemmas that existing automatic solvers can already prove were excluded so the benchmark focuses on reasoning that current automation does not handle.

What would settle it

Give a strong automated prover, or a human expert, access to all 1,329 verified lemmas as an allowed library and ask it to prove the 13 full IMO statements. If a system that proves essentially all the lemmas still cannot assemble any full proof, the decomposition is not capturing the reasoning needed. A narrower check is to hide the final step of each proof and see whether models can use the granted lemma to finish, which the chained lemmas in the dataset already make possible.

Watch

Extended reading notes

Core claim

The central claim is that a hard IMO proof can be rewritten as a graded collection of small, individually checkable lemmas, and that current AI systems still fail on most of these small pieces. The paper contributes complete Lean 4 proofs for 17 IMO problems that previously had no public Lean proof, and for 13 of those problems it extracts 1,329 lemmas, each with a proof verified by Lean, totaling more than 40,000 lines of formal code. On this lemma dataset the best evaluated model proves 522 of 1,329 lemmas (39.3%), o3-mini after feedback proves 316 (23.8%), and the successful proofs produced by specialized provers are almost all short (at most 15 lines), although many human-written lemma proofs are considerably longer. The paper interprets this as evidence that the current bottleneck is less about executing individual proof steps and more about planning and sustaining long proof chains.

Load-bearing premise

The central claim depends on the assumption that the manually chosen 1,329 lemmas genuinely are the building blocks of the IMO proofs, so a model's success on them measures its ability to prove the full problems.

Editorial extensions

If this is right

  • Every IMO problem in the miniF2F test set now has a public Lean proof, so future evaluations can be checked against ground truth instead of missing or altered formalizations.
  • The 1,329 lemmas give a graded benchmark: a model that cannot prove the small pieces has no credible claim to solving the full problems, while a model that proves the pieces but not the whole proof exhibits a specific planning deficit.
  • The near-zero accuracy of specialized provers on lemmas whose proofs exceed 10-15 lines identifies long proof chains, not single-tactic steps, as the main thing to improve.
  • The paper's error labels (hallucination, wrong approach, wrong implementation, incomplete proof, minor error) give a repeatable vocabulary for diagnosing why a generated Lean proof fails.
  • Because the dataset is public and machine-checked, model developers can use it as a shared benchmark while keeping the full IMO proofs out of training to avoid contamination.

Reading between the lines

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

  • A natural extension, not run in the paper, is to fine-tune an open model on the 1,329 lemmas while withholding the 13 full proofs, then measure transfer to the full IMO statements; success would confirm the building-block hypothesis, and failure would localize the bottleneck as assembly rather than execution.
  • The same decomposition recipe could be applied to other long formal proofs to generate curricula for any proof library, and the paper's bounds on how many lemmas can be extracted from n lines of proof give a rough cost model for doing so.
  • The large gap between general-purpose math models (1 lemma proved) and Lean-specialized provers (roughly 30-40%) suggests that formal-language competence is a distinct skill from informal mathematical reasoning, so hybrid systems pairing a general reasoner with a specialized proof search may be a faster route than one model doing everything.
  • The benchmark's difficulty will erode as automatic solvers improve, since lemmas solvable by linarith, omega, ring, and similar tactics were deliberately excluded; re-running the decomposition on newer IMO problems would keep the benchmark meaningful.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 6 minor

Summary. The paper contributes original Lean 4 formal proofs for 17 IMO problems that previously lacked public Lean proofs, of which 14 are from the miniF2F test set and 3 are from IMO 2022 and 2023. From 13 of these proofs the authors extract a dataset of 1,329 lemmas (about 40k lines of Lean code) and evaluate six LLM-based provers on it, reporting accuracies between 0% and 39.3%. The paper also provides a detailed manual error taxonomy for o3-mini's failed proofs, including hallucination, wrong approach, wrong implementation, incomplete proof, and minor errors. All formal proofs and lemmas are machine-checked in Lean 4.17, and the dataset and code are released on GitHub.

Significance. If the claims hold, this is a valuable community resource: it supplies verified Lean proofs for hard IMO problems that were missing from the public domain, and it provides a sizable, machine-checked lemma set for evaluating and diagnosing automated theorem provers. The evaluation is informative because it covers multiple models, includes open and closed training-set regimes, and reports human-reviewed error categories. The paper's central limitation is the unclear composition of the 1,329 lemmas: Section 4.1 explicitly creates both standalone lemmas and hypothesis-granting variants, but the paper never reports how many of the 1,329 are of each type, which affects the interpretation of the headline accuracies as a measure of performance on the 'building blocks' of IMO proofs. The machine-checked existence of the proofs is not in question.

major comments (2)
  1. [§4.1, Lemmas 5–8] The decomposition procedure creates two structurally different kinds of lemmas: standalone intermediate facts (Lemmas 1–4 in the example) and variants that grant some of those facts back to the original problem (Lemmas 5–8). The paper says the examples lead to 2*k lemmas per proof, meaning a large share of the dataset could consist of hypothesis-granting, context-specific proof-state snapshots rather than independent mathematical building blocks. The paper never reports the fraction of such variants in the 1,329 lemmas, nor does it report accuracies separately for the standalone subset. This is load-bearing for the benchmark claim: aggregate accuracies in Tables 2, 3, and 5 conflate the ability to discover a fact with the ability to use a granted hypothesis. Please add a breakdown by lemma type and show that the main conclusions (low absolute accuracy, length-based failure patterns, and problem-level rankings) are robust when only distinct standalone target statements are counted.
  2. [§4.1 and §4.2] The paper describes the decomposition as a 'method' and derives formal bounds, but the actual selection of which intermediate hypotheses to turn into lemmas, and which granted variants to include, is made by human judgment and is not specified algorithmically. The datasheet in Appendix H also states that lemmas provable by certain automatic solvers were excluded. As a result, the 1,329 lemmas are not a reproducible, exhaustive decomposition of the 13 proofs, and the dataset's coverage of the proof space is unclear. The authors should state explicitly which choices were made, provide the code or criteria used to identify intermediate hypotheses, and discuss how the exclusion of solver-provable lemmas affects the dataset's claim to represent the 'building blocks' of these IMO problems.
minor comments (6)
  1. [Abstract; §1.4; Table C2] The number of lines of Lean proof is given as 5,880 in the abstract, 5,790 in Section 1.4, and 5,884 in Table C2; these should be reconciled.
  2. [Introduction; Table 1; Table D3] The introduction states the dataset has 1,330 lemmas, while the abstract, Table 1, and Table D3 all report 1,329; please correct the inconsistency.
  3. [Table 5; Table E4] The DeepSeek-Prover total differs between Table 5 (522, 39.3%) and Table E4 (523, 39.4%); the same evaluation should yield a single count.
  4. [§1.4] There is a typo in 'stat-of-the-art'; it should read 'state-of-the-art'.
  5. [§4.2] The phrase 'derive an upper bound' is imprecise because the expressions (n−2)+(n−2)+(n−3) are exact counts for the described forward/backward procedures, not an upper bound over all possible decompositions.
  6. [Appendix H, 'Are there any errors...'] The datasheet's categorical 'No' regarding errors and redundancies is stronger than what machine-checking establishes: Lean verifies the formal statements and proofs as written, but it does not verify that the lemmas are the intended cognitive 'building blocks' or that they are non-redundant in the proof's reasoning.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the formal proofs are machine-checked, the lemma dataset is constructed from those proofs, and the LLM evaluations are external benchmark measurements; no central claim reduces to its inputs.

full rationale

The paper's central contributions are (1) original Lean 4 formal proofs for IMO problems, (2) a dataset of 1,329 lemmas obtained by decomposing 13 of those proofs, and (3) evaluations of external LLMs on that fixed dataset. Each link in this chain is supported by an independent check: the proofs and lemmas are verified by the Lean theorem prover against Mathlib, and every LLM accuracy number is determined by whether the model's output compiles in Lean. No parameter is fitted to the benchmark, and no reported accuracy is derived from an input quantity that already contains it. The decomposition procedure in Section 4.1 does create hypothesis-granting lemma variants (e.g., granting lemmas 1,2,3,4 to the original problem), but those are dataset-construction choices, not circular derivations: the paper does not claim that solving such variants entails solving the original IMO problem, and the aggregate accuracy figures are measurements of the fixed dataset as constructed. The interpretation that lemmas are 'building blocks' or 'stepping stones' is a stated design goal and an evaluation-diagnostic claim, not a theorem derived from the lemma counts by construction. There is also no load-bearing self-citation: the references to Goedel-Prover, DeepSeek-Prover, ReProver, and o3-mini are external systems whose outputs are independently checked by Lean, and the paper makes no uniqueness claim imported from the authors' prior work. Appendix A candidly limits the contribution to building blocks and notes that planning remains needed, but this is a scope limitation rather than an admission of circularity. The skeptical concern that some lemmas are proof-state snapshots rather than independent mathematical facts is a benchmark-validity question, not a circularity question, because the paper's reported measurements would remain true of the fixed dataset regardless of how representative those lemmas are.

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

The central claim depends only on the existence of verified Lean proofs and a dataset. No new physical or mathematical entities are introduced. The only background assumption is the reliability of Lean and Mathlib.

assumptions (1)
  • domain assumption Lean 4.17 and Mathlib are sound as a proof-checking system
    The paper relies on Lean's verification for the correctness of all formal proofs and lemmas (Section 2 and Appendix H). This is standard for the field but unproved in the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems." pith.science (2026). https://pith.science/paper/DQST3VNV

@misc{pith2026241118872,
  author       = {Pith},
  title        = {Pith review of: A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DQST3VNV}},
  note         = {Machine review of arXiv:2411.18872}
}
read the original abstract

Using AI to write formal proofs for mathematical problems is a challenging task that has seen some advancements in recent years. Automated systems such as Lean can verify the correctness of proofs written in formal language, yet writing the proofs in formal language can be challenging for humans and machines. The miniF2F benchmark has 20 IMO problems in its test set, yet formal proofs are available only for 6 of these problems (3 of which are only written by mathematicians). The model with best accuracy can only prove 2 of these 20 IMO problems, from 1950s and 60s, while its training set is a secret. In this work, we write complete, original formal proofs for the remaining IMO problems in Lean along with 3 extra problems from IMO 2022 and 2023. This effort expands the availability of proof currently in the public domain by creating 5,880 lines of Lean proof. The goal of the paper is to pave the way for developing AI models that can automatically write the formal proofs for all the IMO problems in miniF2F and beyond by providing an evaluation benchmark. In this pursuit, we devise a method to decompose the proofs of these problems into their building blocks, constructing a dataset of 1,329 lemmas with more than 40k lines of Lean code. These lemmas are not trivial, yet they are approachable, providing the opportunity to evaluate and diagnose the failures and successes of AI models. We evaluate the ability of the SOTA LLMs on our dataset and analyze their success and failure modes from different perspectives. Our dataset and code is available at: https://github.com/roozbeh-yz/IMO-Steps.

Figures

Figures reproduced from arXiv: 2411.18872 by the authors.

Figure 1
Figure 1. While o3-mini fails to write the correct proof for most of the 1-liners, it does considerably better [PITH_FULL_IMAGE:figures/full_fig_p009_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

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

  1. Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models

    cs.AI 2025-06 conditional novelty 6.0 of 10

    An inference-only neuro-symbolic pipeline, DSP+, solves 80.7% of miniF2F and the previously unsolved imo_2019_p1, matching heavily RL-trained theorem provers without fine-tuning.

Reference graph

Works this paper leans on

31 extracted references · 10 canonical work pages · cited by 1 Pith paper

  1. [1]

    Sparks of artificial general intelligence: Early experiments with GPT-4

    S \'e bastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, et al. Sparks of artificial general intelligence: Early experiments with GPT-4 . arXiv preprint arXiv:2303.12712, 2023

    arXiv 2023

  2. [2]

    Mathematical reasoning and the computer

    Kevin Buzzard. Mathematical reasoning and the computer. Bulletin of the American Mathematical Society, 2024

    2024

  3. [3]

    A Lean proof of Fermat’s Last Theorem

    Kevin Buzzard and Richard Taylor. A Lean proof of Fermat’s Last Theorem . Technical report, Imperial College of London, 2024. https://imperialcollegelondon.github.io/FLT/blueprint.pdf

    work page 2024

  4. [4]

    Cedar: A new language for expressive, fast, safe, and analyzable authorization

    Joseph W Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, et al. Cedar: A new language for expressive, fast, safe, and analyzable authorization. Proceedings of the ACM on Programming Languages, 8: 0 670--697, 2024

    work page 2024

  5. [5]

    The Lean theorem prover (system description)

    Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In 25th International Conference on Automated Deduction, pp.\ 378--388, 2015

    work page 2015

  6. [6]

    ImageNet : A large-scale hierarchical image database

    Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. ImageNet : A large-scale hierarchical image database. In IEEE Conference on Computer Vision and Pattern recognition, pp.\ 248--255, 2009

    work page 2009

  7. [7]

    The Llama 3 herd of models

    Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The Llama 3 herd of models. arXiv preprint arXiv:2407.21783, 2024

    arXiv 2024

  8. [8]

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

    Emily First, Markus 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

Show all 31 references
  1. [9]

    Datasheets for datasets

    Timnit Gebru, Jamie Morgenstern, Briana Vecchione, Jennifer Wortman Vaughan, Hanna Wallach, Hal Daum \'e III, and Kate Crawford. Datasheets for datasets. Communications of the ACM, 64 0 (12): 0 86--92, 2021

    2021

  2. [10]

    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 Repr...

    2022

  3. [11]

    Large language models are zero-shot reasoners

    Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners. Advances in Neural Information Processing Systems, 35: 0 22199--22213, 2022

    2022

  4. [12]

    Hypertree proof search for neural theorem proving

    Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems, 2022

    2022

  5. [13]

    Let's verify step by step

    Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let's verify step by step. In The Twelfth International Conference on Learning Representations, 2023

    2023

  6. [14]

    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

    2025 arXiv

  7. [15]

    OpenAI o3-mini, January 2025

    OpenAI. OpenAI o3-mini, January 2025. URL https://openai.com/index/openai-o3-mini/

    2025

  8. [16]

    Kasparov and Deep Blue: The historic chess match between man and machine

    Bruce Pandolfini. Kasparov and Deep Blue: The historic chess match between man and machine. Simon and Schuster, 1997

    1997

  9. [17]

    OpenWebMath : An open dataset of high-quality mathematical web text

    Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, and Jimmy Ba. OpenWebMath : An open dataset of high-quality mathematical web text. In The Twelfth International Conference on Learning Representations, 2023

    2023

  10. [18]

    Formal mathematics statement curriculum learning

    Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In The Eleventh International Conference on Learning Representations, 2022

    2022

  11. [19]

    Do ImageNet classifiers generalize to ImageNet ? In International Conference on Machine Learning, pp.\ 5389--5400, 2019

    Benjamin Recht, Rebecca Roelofs, Ludwig Schmidt, and Vaishaal Shankar. Do ImageNet classifiers generalize to ImageNet ? In International Conference on Machine Learning, pp.\ 5389--5400, 2019

    2019

  12. [20]

    Mathematical discoveries from program search with large language models

    Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M Pawan Kumar, Emilien Dupont, Francisco JR Ruiz, Jordan S Ellenberg, Pengming Wang, Omar Fawzi, et al. Mathematical discoveries from program search with large language models. Nature, 625 0 (7...

    2024

  13. [21]

    Mastering the game of Go without human knowledge

    David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of Go without human knowledge. Nature, 550 0 (7676): 0 354--359, 2017

    2017

  14. [22]

    Towards large language models as copilots for theorem proving in Lean

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

    2024 arXiv

  15. [23]

    Solving Olympiad geometry without human demonstrations

    Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving Olympiad geometry without human demonstrations. Nature, 625 0 (7995): 0 476--482, 2024

    2024

  16. [24]

    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

  17. [25]

    DeepSeek-Prover : Advancing theorem proving in LLMs through large-scale synthetic data

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover : Advancing theorem proving in LLMs through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024 a

    2024 arXiv

  18. [26]

    Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search

    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 b

    2024 arXiv

  19. [27]

    Qwen2.5-math technical report: Toward mathematical expert model via self-improvement

    An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, et al. Qwen2.5-math technical report: Toward mathematical expert model via self-improvement. arXiv preprint arXiv:2409.12122, 2024

    2024 arXiv

  20. [28]

    LeanDojo : Theorem proving with retrieval-augmented language models

    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. In Thirty-seventh Conference on Neural Information Processing Systems Datasets an...

    2023

  21. [29]

    Skill-Mix : a flexible and expandable family of evaluations for ai models

    Dingli Yu, Simran Kaur, Arushi Gupta, Jonah Brown-Cohen, Anirudh Goyal, and Sanjeev Arora. Skill-Mix : a flexible and expandable family of evaluations for ai models. In The Twelfth International Conference on Learning Representations, 2023

    2023

  22. [30]

    miniF2F : A cross-system benchmark for formal Olympiad-level mathematics

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F : A cross-system benchmark for formal Olympiad-level mathematics. In International Conference on Learning Representations, 2021

    2021

  23. [31]

    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...

Pith tools

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