Update READMEs, leaderboard, Coq dataset

README.md

@@ -6,41 +6,37 @@
     <a href="https://arxiv.org/abs/2407.11214"><img src="https://img.shields.io/badge/arXiv-2407.11214-b31b1b.svg"></a>
 </p>
 
-PutnamBench is a benchmark for evaluation of theorem-proving algorithms on competition mathematics problems sourced from the William Lowell Putnam Mathematical Competition years 1962 - 2023. Our formalizations currently support three formal languages : Lean 4 $\land$ Isabelle $\land$ Coq. PutnamBench comprises of 1697 manually-crafted formalizations, aggregated over all languages.
+PutnamBench is a benchmark for evaluation of theorem-proving algorithms on competition mathematics problems sourced from the William Lowell Putnam Mathematical Competition years 1962 - 2023. Our formalizations currently support three formal languages : Lean 4 $\land$ Isabelle $\land$ Coq. PutnamBench comprises of 1696 manually-crafted formalizations, aggregated over all languages.
 
 PutnamBench aims to support research in automated mathematical reasoning by providing a multilingual benchmark for evaluating theorem-proving algorithms. It is released under permissive licenses (Apache 2.0 for Lean 4 and Isabelle, MIT for Coq). The [informal statements](informal/README.md) are also available with permission from the MAA.
 
 PutnamBench includes factored solutions for problems which require exhibiting a numerical answer in addition to its proof of correctness. For these problems, one can attempt two tasks: proving the problem with the numerical answer written into the theorem statement, or additionally producing the answer along with the proof.
 
 We are hosting a [**leaderboard**](https://trishullab.github.io/PutnamBench/leaderboard.html) and will readily receive evaluation results which are accompanied by a preprint or publication. **Do not** include proofs as confirmation in any public setting. Please reach out privately at `[email protected]` with any requests for additions to the leaderboard. 
 
-**We strongly encourage community feedback!** Please let us know if you have any comments for improving PutnamBench. If you notice any mistakes, please raise an issue on the repository and we will address it. We kindly ask that you do not write formal proofs for any of the problems in an effort to reduce contamination.
+**We strongly encourage community feedback!** Please let us know if you have any comments for improving PutnamBench. If you notice any mistakes, please raise an issue on the repository and we will address it. We kindly ask that you do not write formal proofs for any of the problems in an effort to reduce contamination. If you do wish to write formal proofs for a subset of the problems, we please ask that you first engage in discussion with us.
 
 ## Statistics 
 | Language      | Count          |
 | ------------- | -------------- |
-| Lean 4        | 640            |
+| Lean 4        | 644            |
 | Isabelle      | 640            |
-| Coq           | 417            |
+| Coq           | 412            |
 
 We also report the number of problems in a certain category. Note that some problems fall under multiple categories. While the categories are intended to capture general features of the problems, we also note that there is a high variance of problems inside an individual category.
 
 | Category         | Total Quantity | 
 | ---------------- | -------------- | 
 | Algebra          | 253            | 
 | Analysis         | 226            |
-| Number Theory    | 107            | 
-| Geometry         | 68             |
+| Number Theory    | 108            | 
+| Geometry         | 69             |
 | Linear Algebra   | 51             | 
 | Abstract Algebra | 28             |  
-| Combinatorics    | 26             | 
-| Probability      | 9              | 
+| Combinatorics    | 29             | 
+| Probability      | 10              | 
 | Set Theory       | 8              | 
 
-## Versioning
-- Version: `v0`
-- In preliminary release to allow for initial community feedback. We seek to release an official first version following several weeks of discussion with the community.
-
 ## Citation
 The associated paper for PutnamBench is [available at this link](https://arxiv.org/abs/2407.11214). Please consider including the following citation if you find PutnamBench useful.
 ```

coq/README.md

@@ -1,6 +1,5 @@
-Note: We are continuing to make modifications to the Coq formalizations, in particular those which were recently added. We encourage feedback, but keep this in mind. The format of the formalizations will be standardized with the other languages upon completion.
+Note that roughly half of the Coq formalizations rely on Mathcomp, while the other half rely on a combination of the Coq Standard Library, Coquelicot, and other various Coq repositories. We also note that while the dependencies listed in each formalization are sufficient to *state* the problem, one may need further mathematical theory developed in Coq to write a proof.
 
-We also note that while the dependencies listed in each formalization are sufficient to *state* the problem, one may need further mathematical theory developed in Coq to write a proof.
 # Installation
 
 You need to install `opam` and then run `setup.sh` to install the necessary dependencies.

coq/src/putnam_1985_a6.v

@@ -0,0 +1,17 @@
+From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import reals.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Open Scope ring_scope.
+
+Variable R : realType.
+Definition putnam_1985_a6_solution : {poly R} := 6 * 'X ^ 2 + 5 * 'X + 1.
+Theorem putnam_1985_a6
+    (Gamma : {poly R} -> R := fun p => \sum_(i <- p) (i ^+ 2))
+    (f : {poly R} := 3 * 'X ^ 2 + 7 * 'X + 2)
+    : let g := putnam_1985_a6_solution in
+      g.[0] = 1 /\ forall n : nat, ge n 1 -> Gamma (f ^ n) = Gamma (g ^ n).
+Proof. Admitted.

docs/results.json

@@ -91,5 +91,15 @@
       "size": 7,
       "condensed-compute-budget": "pass@4096",
       "note": "pass@2048 w/ T = 1.0 + pass@2048 w/ T = 0.7"
+    },
+    "ABEL": {
+      "link": "https://openreview.net/forum?id=kk3mSjVCUO",
+      "open-data": "NONE",
+      "num-solved": {
+        "lean-wsolution": 7
+      },
+      "size": 7,
+      "condensed-compute-budget": "pass@596",
+      "note": "7 hour cumulative online proof search on 256 GPUs"
     }
 }

informal/README.md

@@ -8,3 +8,5 @@ that is, you must write:
 
 These statements are also present in the docstrings of some of the formal statements.
 Github CI will automatically catch if these are out of sync, but if you update them in one place you will have to update them in the other.
+
+When a problem happens to require a solution (i.e. some additional data requested in the problem statement), we also add an `informal_solution` field which has as value an imperative sentence roughly of the form "Show that the solution is ..."