This dataset was made with Curator.
A sample from the dataset:
{
"name": "putnam_1981_a1",
"lean4_statement": "abbrev putnam_1981_a1_solution : \u211d := sorry\n-- 1/8\ntheorem putnam_1981_a1\n(P : \u2115 \u2192 \u2115 \u2192 Prop := fun n k : \u2115 => 5^k \u2223 \u220f m in Finset.Icc 1 n, (m^m : \u2124))\n(E : \u2115 \u2192 \u2115)\n(hE : \u2200 n \u2208 Ici 1, P n (E n) \u2227 \u2200 k : \u2115, P n k… See the full description on the dataset page:
https://huggingface.co/datasets/mlfoundations-dev/putnam_bench_r1.
