PutnamBench: A Multilingual Competition-Mathematics Benchmark for Formal Theorem-Proving

Authors: george  tsoukalas
jasper  lee
john  jennings
jimmy  xin
michelle  ding
michael  jennings
amitayush  thakur
swarat  chaudhuri
Venue: ICML_cc_2024_Workshop_AI4MATH
Published: 2024-06-01 05:59:19

Abstract: We present PutnamBench, a new multilingual evaluation benchmark for formal theorem-proving. PutnamBench consists of formalizations of problems sourced from the William Lowell Putnam Mathematical Competition, the premier undergraduate-level mathematics competition in North America. All the problem statements come with formalizations in Lean 4 and Isabelle; a substantial subset have Coq formalizations as well. PutnamBench consists of 1337 hand-written formalizations across the three proof assistants, and aims to benchmark the next generation of theorem-proving algorithms for competition mathematics.  Proving the theorems requires significant problem-solving ability and proficiency in a broad range of topics taught in undergraduate mathematics courses. We evaluate several established neural and symbolic theorem provers using PutnamBench. These approaches can only solve a handful of the problems, establishing our benchmark as a difficult open challenge for research on formal theorem-proving. PutnamBench is available at https://github.com/trishullab/PUTNAM.

Main paper: 
 introduction: 
 Automating mathematical reasoning is a longstanding goal in artificial intelligence. A prominent line of work on the problem focuses on developing algorithms to produce proofs in formal frameworks like Lean. These frameworks can "execute" proofs like code, giving a high-confidence signal as to correctness, and offer execution feedback, which can be used to improve the quality of generated proofs. research area. The two most prominent datasets for benchmarking theorem-proving methods for competition mathematics are MINIF2F (Zheng et al., 2021) and FIMO (Liu et al., 2023) . The former formalizes problems drawn from high-school mathematics competitions; the latter consists of a collection of International Mathematics Olympiad (IMO) shortlist problems. Both benchmarks have limitations. For example, MINIF2F contains many "simple" problems that can be immediately solved using an SMT-solver, and FIMO only targets the Lean 3 framework, which is no longer actively maintained.More generally, as large language models (LLMs) grow in importance as a tool for neural theorem-proving, preventing leakage from pretraining sets and evaluation sets is more important than ever. This makes the continued supply of new benchmarks an important goal.In this paper, we respond to this challenge with PUTNAM-BENCH, a new multilingual benchmark for neural theoremprovers. PUTNAMBENCH includes formalizations of 514 problems appearing in the William Lowell Putnam Mathematical Competition, a premier college-level mathematics competition in the United States, between 1962 and 2023. All our problems have a Lean 4 and Isabelle formalization; a substantial fraction have formalizations in Coq as well -a first for competition mathematics benchmarks for theorem-proving. PUTNAMBENCH totals 1337 hand-crafted formalizations across the three interactive theorem provers.One key benefit of PUTNAMBENCH is that the Putnam competition problems require a broad base of mathematical knowledge and skills. In particular, because they target undergraduate students, they cover topics such as analysis and abstract algebra that do not appear in the International Mathematics Olympiad (IMO), a high school competition. At the same time, success in the two competitions is correlatedwinners of the Putnam competition are often IMO medalists as well. Hence, we assert that PUTNAMBENCH is aligned with the IMO Grand Challenge and the AI Mathematical Olympiad Prize, which are challenges for the research community to develop a theorem-proving algorithm which can attain a gold medal at the IMO. The proof introduces all relevant variables and hypotheses with intro, indicates the choice of x, y, z with use, and then solves all goals using automated tactics like linarith and ring. This proof was discovered through a few-shot invocation of GPT-4o.We use PUTNAMBENCH to evaluate several neural and symbolic approaches: Draft-Sketch-Prove (Jiang et al., 2022b) , COPRA (Thakur et al., 2024) , GPT-4, Sledgehammer (Paulson & Blanchette, 2015) , and Coqhammer (Czajka & Kaliszyk, 2018) . Collectively, these methods can only solve a handful of the PUTNAMBENCH problems, establishing PUTNAMBENCH as a hard open challenge for the neural theorem-proving community. 
background: 
 Formal Theorem-Proving. Formal proof frameworks like Lean 4 (Moura & Ullrich, 2021) , Coq (Huet et al., 1997) , and Isabelle (Wenzel et al., 2008) allow users to write machine-verifiable proofs of mathematical theorems.To create such a proof, one first uses a framework-specific language to formally state the target theorem. The mathematical objects referenced in the theorem can be imported from an existing repository or defined by the user. During the proof process, the proof framework maintains a state that includes information about the parts of the proof that remain to be completed. One can change this state by executing a proof step. The user's goal is to write a sequence of proof steps (in the framework's language) that changes the proof state to a special state "QED" in which there are no unmet proof obligations.Figure 1 illustrates a theorem and proof in the Lean 4 framework.The Putnam Competition. The William Lowell Putnam Mathematical Competition, organized by the Mathematical Association of America (MAA), is the premier collegiate mathematics competition in North America. Thousands of undergraduate students from universities across the United States and Canada take the exam each year. The competition comprises two 3-hour-long sessions of six problems each, presented in approximately ascending order of difficulty within each session. While some problems require competitors to furnish a concrete solution (such as a number, a set, or the truth value of a given statement), all problems require a natural-language proof of correctness. The contest draws from a wide variety of topics in the undergraduate curriculum, often using instances of ideas from research-level mathematics. 
putnambench: 
 PUTNAMBENCH is a multilingual evaluation benchmark consisting of formalized problems from the Putnam compe- Generally, the formalizations of the problems are aligned in their structure, including hypothesis naming and framing. Differences may arise according to the underlying foundations of each language. We also note that the pre-defined mathematical theory in each language differs, which can sometimes lead to difficulties formalizing certain problems.Compared to the prior benchmarks MINIF2F, FIMO, and PROOFNET, PUTNAMBENCH is the first to support Lean 4 on initial release * .Factored solutions. Roughly 60% of Putnam problems, in their natural language form, require exhibiting a (closedform) solution along with a proof of its correctness. Such problems are not immediately formalizable as they are not directly the statement of a theorem. Prior benchmarks such as MINIF2F sidestep this issue by rewording the problem statement to ask for a proof that the solution satisfies the constraints of the problem. However, this reduction diminishes the overall difficulty of the problem, as producing a solution can constitute the majority of its difficulty. To address this issue, we factor solutions out of such problems from the formalized theorem statement. We include examples in the Appendix A. In this way, we provide two tasks for neural theorem proving:• Task 1: Given the theorem statement, first identify the (closed-form) solution, and then provide a proof of correctness by rewriting the solution into the theorem statement.• Task 2: Given the theorem statement and solution, * MINIF2F, FIMO, and PROOFNET were originally released using Lean 3, and some have been updated to include Lean 4 formalizations following community efforts Azerbayev et al. (2023) ; Vishwakarma et al. (2024) .produce a proof of its correctness. This task aligns with the current benchmarks.In this way, our formalizations can reflect the true difficulty of the informal problem statement. We note that the process of producing the numerical solution may be highly correlated with the proof of its correctness.Additionally, we mention that much like ProofNet, PUT-NAMBENCH can be applied for measuring autoformalization capabilities of current LLMs. We believe such investigations can be especially enlightening towards understanding the ability of LLMs to combine concepts from multiple domains.Formalization effort and challenges. Our formalization effort was carried out over several months and was performed by a group of graduate students and undergraduate students with experience in both university mathematics and computer science. We found that the average time-toformalize a single problem in one language was roughly 25 minutes. Each formalization was verified at least once, and we measured that the verification of a single formalization took 10 minutes on average. We acknowledge that the timeto-formalize we report is higher than that of MINIF2F; we believe this is largely due to the increased complexity of the Putnam problems, which oftentimes require definitions we must locate in each language's respective mathematical libraries.We first produced formalizations in Lean 4, and then proceeded with our formalization effort in Isabelle and then Coq † . Due to differences in the underlying foundations of each language, we found that formalizations in one language sometimes do not directly transfer to another; for example, Isabelle does not have a subtyping mechanism, which we made extensive use of in Lean 4. Formalizations in Coq had an added difficulty: Coq lacks an expansive unified library such as Mathlib and the HOL Library, which we make extensive use of in Lean 4 and Isabelle respectively. Our Coq formalizations rely on eight mathematics repositories: Stdlib, Mathcomp, Mathcomp-analysis, Coquelicot, Stdpp, † PUTNAMBENCH currently features 309 formalizations in Coq and continues to expand as we navigate formalization obstacles specific to Coq.(a) theorem putnam_2006_b2 (n : N) (npos : n > 0) (X : Finset R) (hXcard : X.card = n) : (∃ S ⊆ X, S ̸ = ∅ ∧ ∃ m : Z, |m + Σ s in S, s| ≤ 1 / (n + 1)) (b) theorem putnam_2006_b2:fixes n :: nat and X :: "real set" assumes npos: "n > 0" and hXcard: GeoCoq, Coqtail, and Coqeal. Some problems may require definitions from multiple of these repositories, which can be incompatible."finite X ∧ card X = n" shows "∃ S ⊆ X. (S ̸ = {}) ∧ (∃ m :: int. ¦m + (Σ s ∈ S. s)¦ ≤ 1 / (n + 1))" (c) Theorem putnam_2006_b2: forall (n: nat) (X: list R) , length X = n -> exists (presS: R -> Prop) (m: Z) (S: list R), (forall (x: R), In x S <-> (In x X /\ presS x)) /\ Rabs (IZR m + (fold_left Rplus S 0)) <= 1 / INR (n + 1).Some problems are not naturally amenable to formalization. We found that while formalizing problems involving probability is possible, such formalizations often require heavy probability theory which does not reflect the spirit of the informal problem statement. Similarly, support for problems involving Euclidean geometry varies among each language; for example, Lean 4 does not yet have a sufficiently extensive library to make most geometry problems formalizable. By contrast, Coq has an extensive geometry repository called GeoCoq, which we utilize in our Coq formalizations.Licensing and Rules of Engagement. PUTNAMBENCH is available under an Apache 2.0 license for Lean 4 and Isabelle, and under an MIT license for Coq. We align the licenses with those of the repositories we use for each language. With permission from the Mathematical Association of America, we also include the informal statements as sourced from the official Putnam archives (Alexanderson et al., 1985; Kedlaya et al., 2002; 2020) . 
experimental evaluation: 
 To understand the challenges that PUTNAMBENCH poses for state-of-the-art theorem-proving approaches, we attempt to solve its problems using a suite of such approaches. Given the relative lack of tailored systems for multilingual theoremproving, we run evaluations for each language separately. Any method that is evaluated on multiple languages is based on off-the-shelf foundation models.Metrics. Our evaluation is based on the pass@n (Lample et al., 2022) metric. This metric measures a prover's ability to produce a successful proof, as determined by the formal proof environment, given a budget of n proof attempts. In search-based methods (Thakur et al., 2024) , each proof attempt involves a distinct search that can query a neural model multiple times.Models. For each of the languages, we perform evaluations using GPT-4 (OpenAI, 2023) ‡ , a highly capable foundation model. We run evaluations using in-context learning, appending several examples of successful proofs of simple theorems in each language. For evaluations with Lean 4 approaches, we note that many approaches have targeted Lean 3, which is not backward-compatible and no longer actively maintained. We additionally evaluate COPRA (Thakur et al., 2024) on PUTNAMBENCH, modifying the prompt examples of COPRA to enable search in Lean 4.For our Isabelle experiments, we run evaluations of Draft, Sketch, and Prove (DSP) (Jiang et al., 2022b) using GPT-4 as the underlying foundation model, noting that many further works for theorem-proving in Isabelle have extended on the DSP pipeline as we mention in Section 5. We also run evaluations using stand-alone invocations to Sledgehammer, a powerful symbolic automation tool in Isabelle that relies on calls to external SMT solvers.As for our Coq experiments, prior neural approaches for Coq have mostly targeted software verification tasks, as opposed to competition mathematics. As a result, our Coq experiments use COPRA, which also supports theorem-proving in Coq. We also run evaluations using CoqHammer (Czajka & Kaliszyk, 2018) , a tool similar to Isabelle's Sledgehammer, which makes calls to external constraint solvers.Lean 4. We prompt GPT-4 in a pass@10, setting temperature T = 0. and the generated proof are given in Figure 1 . In particular, Putnam 1988 B1 is solved on the first of 10 attempts. An example of a failure mode of GPT-4 is given in Figure 17 .We also run evaluations with COPRA, using their default hyperparameters for search, performing a pass@1, and allowing 60 queries to GPT-4. However, since COPRA was originally designed for interaction with Lean 3, we modify its system prompt to enable search in Lean 4. The result of the step-wise proof search over all Lean 4 formalizations yields a correct proof to one problem (1988 B1). We find that backtracking in the search was not required for this proof, which was 10 lines long and was found at the 10th query. It is possible that affording COPRA further queries to GPT-4 can yield more successful proofs, though it is not yet feasible to perform such an experiment due to the cost of queries to GPT-4.We found that, by default, GPT-4 produces proofs using Lean 3 syntax, which is not compatible with Lean 4. Even when directed to produce outputs in Lean 4, GPT-4 typically continues to produce outputs in Lean 3. Our prompt, which we include in Figure 15 , elucidates some design differences in Lean 4 to better enforce compliance with the Lean 4 syntax. However, we noticed many examples where GPT-4 continues to output terms in Lean 3 syntax. One such example is given in Figure 21 .Isabelle. We run GPT-4 using the same configuration, with modified prompts for Isabelle, on our Isabelle formalizations. We find that GPT-4 is incapable of furnishing successful proofs to any of the problems in PUTNAMBENCH.DSP represents a neurosymbolic methodology which has seen significant application for theorem-proving in MINIF2F. We run DSP with pass@10, using temperature T = 0.1 and GPT-4 as the underlying language model. Our evaluation yields two successful proofs: one of Putnam 2001 A1, a problem involving magmas (sets with a binary operation), and one of Putnam 1995 A1, a problem involving a closed-under-multiplication subset of the reals. In particular, Putnam 1995 A1 cannot be solved by Sledgehammer alone. The generated proof is included in Figure 3 .We run a baseline using Sledgehammer, a powerful automation tool in Isabelle which makes calls to external SMT solvers to prove a given goal. With a set timeout of t = 120 seconds, we run Sledgehammer on each Isabelle formalization. The result of this evaluation is 3 successfully proven problems: Putnam 1971 B1, 2001 A1, and 2012 A2. Notably, all of these problems are statements about sets with binary operations. We include the statements of 1971 B1 and 2012 A2 in Figure 20 .Coq. We run GPT-4 with a Coq-based prompt on our Coq formalizations using the same configuration as in Lean and Isabelle. The result of the experiment is 1 solved problem, namely Putnam 1988 B1, which was also solved in Lean 4. The proof, which we include in Figure 13 , generally follows the same structure as the proof in Lean.An evaluation with COPRA, in a pass@1-with-60-queries and T = 0.0 also yields a successful proof only for Putnam 1988 B1 which we include in Figure 13 . In this case, backtracking was crucial for proof search on this problem. The crucial step in 1988 B1 is the choice of x, y, z once a and b have been introduced. Initially, COPRA predicts the erroneous choice x, y, z = 1, 1, ab -1 and eventually reverts this choice using backtracking. Afterwards, COPRA predicts a correct choice x, y, z = 1, a -1, b -1 and proceeds with the proof.We run CoqHammer with 8 parallel threads using an ATP timeout of 100 seconds, proof reconstruction timeout of 15 seconds, and sauto timeout of 5 seconds, for a total of 120 seconds allocated for each formalization. The evaluation yields no successful proofs -indicating that symbolic tools in Coq are not yet capable of handling PUTNAMBENCH problems. It is not surprising that CoqHammer does not match the performance of Sledgehammer even though they rely on the same external solvers. The underlying logical system of Coq is more complex than that of Isabelle and is hence less amenable to automation.Aggregating over all experiments performed in all languages, we find that a total of 5 problems in PUTNAM-BENCH are successfully proven. A majority of these come from evaluations in Isabelle, particularly with strong contributions from Sledgehammer. Sledgehammer can solve all three problems involving magmas which appear in our benchmark but fails to produce successful proofs for any other formalization. DSP solves an additional problem and relies heavily on Sledgehammer to fill in the proofs of intermediate steps. The single problem solved in Lean and Coq also makes use of automated tactics like linarith and lia, and requires only a single crucial step.Hence, we find that a few PUTNAMBENCH problems are not entirely intractable using current methods. However, anecdotally, these problems are among the easiest ever included in the Putnam competition. All admit a very short natural language proof and do not require reasoning about particularly complicated objects. We believe that significant advancements in automated mathematical reasoning are required to make progress on PUTNAMBENCH. 
related works: 
 Formal Benchmarks. Several evaluation benchmarks for formal mathematics have been developed in recent years. MINIF2F (Zheng et al., 2021) is a formal-to-formal benchmark of competition problems, sourced from high school competitions such as the AMC, AIME, and IMO. MINIF2F is a multilingual benchmark, comprising of 488 problems each formalized in Lean 3, Metamath, Isabelle and HOL Light. We chose not to include formalizations in Metamath and HOL Light as they have not been the focus of attention for neural theorem-proving. A similar competition-style benchmark is FIMO (Liu et al., 2023) , which contains 149 formalizations of IMO shortlist problems in Lean 3, generated automatically using LLMs and then verified via humans. Notably, their provided evaluation with GPT-4 yields no solved problems. This indicates that such problems may be out of the grasp of current techniques. Oftentimes informal problem statements from such competitions require a closed-form solution to be exhibited, and do not ask for a proof-of-correctness. Both benchmarks are designed to measure certifying the solution to the informal problem statement when one exists. Compfiles is a collection of 171 Lean 4 formalizations of competition problems, predominantly from the IMO and USAMO, often accompanied by a formal proof, which has not seen use in benchmarking automated theorem provers. ProofNet (Azerbayev et al., 2023) introduced a benchmark of 371 exercises, formalized in Lean3, from popular textbooks in the standard undergraduate mathematics curriculum. While largely not competitionbased, problems in ProofNet draw from a broader library of concepts than MINIF2F and FIMO, which rely only on high-school mathematics. LeanDojo (Yang et al., 2023) introduces a dataset of formal mathematics and proofs derived from Lean's Mathlib library (mathlib Community, 2020), and trains a retrieval-augmented model towards generating proofs on their held-out test set. ProverBot9001 (Sanchez-Stern et al., 2020) introduced a dataset for theorems and proofs written in Coq derived from CompCert (Leroy, 2009) , a formally verified C compiler. PISA (Jiang et al.) is a dataset derived from Isabelle's Archive of Formal Proofs (Arc), which contains theorems and proofs from general mathematics as opposed to specifically competition problems.Informal Benchmarks. Several popular datasets for benchmarking natural language reasoning for mathematics exist. MATH (Hendrycks et al., 2021 ) is a collection of 12,500 mathematics problems, in natural language only, sourced from various high school competitions additionally supplied with step-by-step informal proofs. MATH is split into a training dataset of 7,500 problems, and a testing split of 5,000 problems. Notably, a "solution" to each problem is an answer, represented as a closed-form numerical value which can be checked against the known value. GSM8K (Cobbe et al., 2021) is a collection of 8,500 grade school mathematics problems, intended to benchmark natural language reasoning for mathematics-style problems. NaturalProofs (Welleck et al., 2021) collects a dataset of informal theorems and proofs scraped from the internet and evaluates transformer-based architectures for retrieval and generation tasks. Lu et al. (2024) introduces a benchmark of 6,141 examples for evaluating visual reasoning for mathematical tasks. While benefiting from the abundance of natural language data, these benchmarks fall short, since in natural language, there is no automatic mechanism for certifiable verification of the reasoning path which yielded the numerical answer. For this reason, metrics for success on these benchmarks usually rely on exact-answer match, because verifying reasoning paths is imprecise and is best done by human experts. By contrast, theorem proving in formal proof assistants comes with a high-confidence signal for correctness of the reasoning path, or proof, of a theorem.Methods for Formal Theorem-Proving. Significant effort has been spent on developing automatic theoremprovers for formal mathematics (Li et al., 2024) . Most recent efforts train a neural module to perform proof-step prediction, which is then wrapped in a search mechanism to locate a valid proof. GPT-f (Polu & Sutskever, 2020) trains a transformer-based architecture on data derived from the Metamath library (Megill & Wheeler, 2019) for proof synthesis. PACT expands on GPT-f by incorporating auxiliary training tasks for the neural module towards theoremproving in Lean 3. FMSCL (Polu et al., 2022) alternates proof-search and training to finetune their neural model based on proofs found during search. HTPS (Lample et al., 2022) uses a transformer-based neural module in an online, MCTS-inspired proof search in Lean 3 and Metamath. CO-PRA (Thakur et al., 2024) uses GPT-4 supplied with error feedback from the environment and lemmas from a retrieval mechanism for an agentic proof-search in Lean 3 and Coq. LLEMMA (Azerbayev et al., 2024) continues pretraining of Code Llama on a mathematics-based corpus dubbed Proof-Pile-2, and uses their learned model for formal proof search in Lean 4. DeepSeek-Prover (Xin et al., 2024) produces synthetic Lean data en-masse for training their prover model. AlphaGeometry (Trinh et al., 2024) targets IMO problems in a geometry-specific proof assistant language using an interleaving search, where a neural module synthesizes auxiliary constructions and a symbolic engine produces deductive closures.The Isabelle proof assistant (Paulson, 1994) , given its declarative nature and powerful symbolic automation, has too been the focus of much attention for neural theorem proving. Isabelle features Sledgehammer (Paulson & Blanchette, 2015) , an automated reasoning tool which calls external automated theorem provers (ATPs) for proof synthesis. Draft, Sketch, Prove (DSP) (Jiang et al., 2022b) uses a high-caliber LLM to generate natural language proofs and converts them into formal sketches in Isabelle, whose gaps are then filled using Sledgehammer. Zhao et al. (2023) employed a diffusion model to predict an optimal ordering of the few-shot examples provided to the LLM in the DSP pipeline. Lyra (Zheng et al., 2023) utilized error-feedback from Isabelle's execution to modify holes in the sketch which were too difficult for the symbolic prover. POETRY (Wang et al., 2024) leverages recursion for theorem-proving and trains a neural module to produce proof sketches, as opposed to using in-context learning with an LLM. LEGO-Prover (Wang et al., 2023) extends the pipeline by incorporating a skill library which grows throughout the proof search task. Separate from approaches utilizing natural language proofs, Thor (Jiang et al., 2022a ) trains a transformer-based architecture to predict successful invocations of Sledgehammer, along with the usual proof-step objective. Baldur (First et al., 2023) explored repairing erroneous proofs in Isabelle through the use of LLMs.The Coq interactive theorem prover has seen use in both software verification and general mathematics. Famously, mechanized proofs of the Four Colour Theorem (Robertson et al., 1997) and the Feit-Thompson theorem (Gonthier et al., 2013a) were produced in Coq. Similarly, numerous software verification projects have been undertaken in Coq, such as CompCert (a formally verified C compiler) and Verdi (Gonthier et al., 2013b ) (a framework for verifying distributed systems protocols). ASTactic (Yang & Deng, 2019) trained a neural module involving recurrent networks and attention on data collected from various Coq repositories. Proverbot9001 (Sanchez-Stern et al., 2020) targeted proof synthesis on a set of held-out theorems from the CompCert project. COPRA (Thakur et al., 2024 ) also evaluates on this CompCert-based task using their multilingual approach. 
conclusion: 
 We presented PUTNAMBENCH, a benchmark for neural theorem-proving consisting of formalizations of Putnam competition problems. A distinctive feature of PUTNAM-BENCH is that it spans a broad range of undergraduate-level mathematical topics, including algebra, analysis, and number theory. Another unique benefit is that it includes problems in Lean 4, Isabelle, and Coq, the three most popular formal proof frameworks.As our experiments show, PUTNAMBENCH is a challenging benchmark: all current theorem-proving approaches fail to solve more than a handful of its problems. We believe that these failures have two root causes: (i) While current theorem-provers can effectively stitch together standard proof steps well-represented in the training corpus, they often fail at synthesizing new lemmas and orchestrating these lemmas into complex proofs. (ii) Current methods often fail to leverage the deep knowledge available in mathematics repositories. Developing a new generation of neural theorem-provers in which these weaknesses are at least partly addressed is an exciting direction of future research. 
impact statement: 
 This paper presents work whose goal is to advance the field of Machine Learning. There are many potential societal consequences of our work, none which we feel must be specifically highlighted here.Putnam 2001 B4. Let S denote the set of rational numbers different from {-1, 0, 1}. Define f : S → S by f (x) = x -1/x. Prove or disprove that ∞ n=1 f (n) (S) = ∅,where f (n) denotes f composed with itself n times. As the problem requires deciding whether the infinite intersection is empty, it is not directly the statement of a theorem. We consider the associated "solution" of this problem to be a boolean value, and factor it out from the theorem statement. sorry is the placeholder keyword for Lean.abbrev putnam_2001_b4_solution : Prop := True theorem putnam_2001_b4 (S : Set Q) (hS : S = univ \ {-1, 0, 1}) (f : S → S) (hf : ∀ x : S, f x = x -1 / (x : Q)) : ∩ n ∈ Ici 1, fˆ[n] '' univ = ∅ ↔ putnam_2001_b4_solution := sorryPutnam 2020 A3. Let a 0 = π/2, and let a n = sin(a n-1 ) for n ≥ 1. Determine whether As the problem requires deciding whether the series converges, it is not directly the statement of a theorem. We consider the associated "solution" of this problem to be a boolean value, and factor it out from the theorem statement.Putnam 1997 A4. Let G be a group with identity e and ϕ : G → G a function such that ϕ(g 1 )ϕ(g 2 )ϕ(g 3 ) = ϕ(h 1 )ϕ(h 2 )ϕ(h 3 ) whenever g 1 g 2 g 3 = e = h 1 h 2 h 3 . Prove that there exists an element a ∈ G such that ψ(x) = aϕ(x) is a homomorphism. The informal statement is slightly underspecified -g 1 , g 2 , g 3 , h 1 , h 2 , h 3 are not explicitly defined to be in G. To produce the formalization, we must be specific about the type of g i , h i .Putnam 2018 B1. Let P be the set of vectors defined byP = a b 0 ≤ a ≤ 2, 0 ≤ b ≤ 100, and a, b ∈ ZFind all v ∈ P such that the set P \ {v} obtained by omitting vector v from P can be partitioned into two sets of equal size and equal sum. While useful for benchmarking straightforward mathematical reasoning in a formal setting, these problems are quite simple compared to the competition problems present in PUTNAMBENCH. We note that MINIF2F does include some formalizations of problems sourced directly from high school competitions, but these are fewer in number.abbrev putnam_2018_b1_solution : Set (Vector Z 2) := {v : Vector Z 2 | ∃ b : Z, 0 ≤ b ∧ b ≤ 100 ∧ Even b ∧ v.toList = [1, b]} theorem putnam_2018_b1 (P : Finset (Vector Z 2)) (v : Vector Z 2) (vinP : Prop) (Pvdiff : Finset (Vector Z 2)) (Pvpart : Prop) (hP : P = {v' : Vector Z 2 | 0 ≤ v'[0] ∧ v'[0] ≤ 2 ∧ 0 ≤ v'[1] ∧ v'[1] ≤ 100}) (hvinP : vinP = (v ∈ P)) (hPvdiff : Pvdiff = P \ ({v} : Finset (Vector Z 2))) (hPvpart : Pvpart = (∃ Q R : Finset (Vector Z 2), (Q ∪ R = Pvdiff) ∧ (Q ∩ R = ∅) ∧ (Q.card = R.card) ∧ (Σ q in Q, q[0] = Σ r in R, r[0]) ∧ (Σ q in Q, q[1] = Σ r in R, r[1]))) : (vinP ∧ Pvpart) ↔ v ∈ putnam_2018_b1_solution := sorryYou  
 
 Appendix: [GOAL] 1 DifferentiableAt R (fun x => g x / hg0 x) 0 → DifferentiableAt R g 0 which gives an operation ⋆ and asserts it is a binary operation on S, also asserts associativity of the operation. The tactic rw [←mul assoc], which performs a rewrite using the associativity of ⋆, is hence not applicable in this setting.Putnam 1995 A1. Let S be a set of real numbers which is closed under multiplication (that is, if a and b are in S, then so is ab. Let T and U be disjoint subsets of S whose union is S. Given that the product of any three (not necessarily distinct) elements of T is in T and the product of any three elements of U is in U , show that at least one of the two subsets T, U is closed under multiplication. then have "∃t1∈T. ∃t2∈T. t1 * t2 / ∈ T" "∃u1∈U. ∃u2∈U. u1 * u2 / ∈ U" by auto then obtain t1 t2 where t1t2: "t1 ∈ T" "t2 ∈ T" "t1 * t2 ∈ U" using hS hunion by blast then obtain u1 u2 where u1u2: "u1 ∈ U" "u2 ∈ U" "u1 * u2 ∈ T" using ¬ ((∀a∈T. ∀b∈T. a * b ∈ T) ∨ (∀a∈U. ∀b∈U. a * b ∈ U)) hS hunion by blast have "t1 * t2 * t3 ∈ T" if "t3 ∈ T" for t3 using hT3 t1t2(1) t1t2(2) that by auto then have "t1 * t2 * t3 ∈ U" if "t3 ∈ T" for t3 using t1t2(3) hS that by (metis disjoint_iff hU3 hdisj mult.commute u1u2(1) u1u2( 2) u1u2( 3)) then have False using hdisj t1t2(1) t1t2( 2) by (meson disjoint_iff_not_equal hT3) then show False by blast qed Figure 18 : A successful proof in Isabelle discovered using DSP. In particular, this proof is not found using a single invocation of sledgehammer, so the sketching mechanism of DSP is crucial for this problem. We note that the DSP pipeline involves using an LLM (GPT-4) to synthesize an informal proof which is translated into a sketch in Isabelle -this can potentially be a source of indirect dataset contamination, as we cannot ensure the informal proofs are not present in GPT-4's training data. [LAST STEP] exists (a -1), 1, (b -1).Figure 21 : Early in COPRA's attempt on Putnam 1988 B1, an incorrect prediction of x, y, z given a, b is made, which dooms that path of search as the most crucial step is the correct choice. Later, at step 32 of search, COPRA backtracks and then successfully predicts a correct choice for x, y, z. Once this step is generated, the remainder of the proof is straightforward. 


Decision: Great paper. It introduces a new dataset at the intersection of formal and informal theorem proving, which can serve as important and challenging benchmarks necessary for increasingly performant LLMs. The paper is well-written, and the creation of the dataset is well-motivated. The only drawback is the lack of baseline experiments on the newly proposed dataset.

Reviews: review: paper_summary: paper_summary: PutnamBench presents a new data at the intersection of formal and informal theorem proving. Notably, the authors' dataset includes problems, of varying difficulty, annotated with proofs spanning a range of languages. The dataset promises to serve as a valuable benchmark and exploratory asset for the field, particularly, around "multilingual" mathematics.
strength_weakness: strength_weakness: The paper should not be rejected. As a minor point of feedback -- I felt that the paper is an interesting case where the related work section is perhaps a bit too long! The subsection on Methods for Formal Theorem Proving was a bit out of place here, as the authors just introduce the data, not actually evaluate said methods. However, that subsection will be useful in a broader piece that does evaluate (or propose new) methods to do well on PutnamBench.
questions: questions: Could the authors please add more details on the students who provided the proofs? Are the authors sure the proofs are "quality"? Are the students maths-students or AI students exposed to formal maths? 

Typo on lines 93-94?
paper_summary: paper_summary: This work introduces a multilingual benchmark for formal theorem proving. The benchmark, called PutnamBench, consists of 421 problems in Lean 4 and Isabelle, and 250 problems in Coq. All problems come from the William Lowell Putnam Mathematical Competition between 1969 and 2023. PutnamBench consists of over 1100 formal theorem proving tasks in total.
strength_weakness: strength_weakness: 1. No baseline performance is provided. We don't know how the strongest baselines (e.g. LEGO-Prover, DeepSeekProver, Lyra, HTPS, etc) will perform on these problems.
questions: questions: Why no performance results are provided? Is it because of time constraint?
paper_summary: paper_summary: The paper introduces PUTNAMBENCH, a benchmark to evaluate neural theorem-provers using over 1100 formalized problems from the William Lowell Putnam Mathematical Competition. It supports Lean 4, Isabelle, and Coq, covering a wide range of undergraduate-level mathematics. PUTNAMBENCH aims to overcome limitations of existing benchmarks by providing diverse and challenging problems, separated solutions, and supporting multiple proof assistants, thus advancing automated theorem-proving research.
strength_weakness: strength_weakness: Lack of Baseline Experiments: The biggest limitation of the paper is the absence of experimental results. There are no baseline experiments showcasing the performance of current LLMs or human performance on PUTNAMBENCH, which is crucial for understanding the benchmark's effectiveness and the current state of theorem-proving capabilities.
questions: questions: 1. What is the current SOTA LLMs' performances on the proposed dataset?