Issues

• Three Lean statements weaker than the problem: putnam_2004_a4 (quantifier scope), putnam_2016_a5 (extra hypotheses), putnam_2003_b4 (real roots only)

  trishullab/PutnamBench#368 · Filter by author AaronY77 opened on Oct 13, 2026

• Informal statements that state a different problem (3 are false as written): 2021_b4, 2013_a3, 2014_b4, 1983_b6

  trishullab/PutnamBench#367 · Filter by author AaronY77 opened on Oct 13, 2026

• putnam_1982_b5 (Lean): operator precedence turns "prove S_x converges" into a hypothesis

  trishullab/PutnamBench#366 · Filter by author AaronY77 opened on Oct 13, 2026

• putnam_2023_a6 (Lean, Isabelle): statement is vacuous — "valid strategy" requires Bob to pick an already-chosen number

  trishullab/PutnamBench#365 · Filter by author AaronY77 opened on Oct 13, 2026

• putnam_2003_a5 (Lean, Isabelle): conclusion asserts an injection, not a one-to-one correspondence

  trishullab/PutnamBench#363 · Filter by author AaronY77 opened on Oct 13, 2026

• putnam_1991_a6 (Lean): hypotheses are inconsistent, statement is vacuous

  trishullab/PutnamBench#361 · Filter by author ZZZamchi opened on Oct 12, 2026

• Suggestion: record a dataset commit pin per leaderboard entry

  trishullab/PutnamBench#353 · Filter by author fabio-rovai opened on Sep 13, 2026

• (669/672) Leaderboard Submission -- Team Humanfia

  trishullab/PutnamBench#339 · Filter by author Lyken17 opened on Jul 17, 2026

• What's the meaning of "no answer" in the leaderboard?

  trishullab/PutnamBench#330 · Filter by author yuanyehome opened on Mar 6, 2026
  2

• Update misformalizations found by Aleph Prover in Isabelle, Rocq

  trishullab/PutnamBench#323 · Filter by author GeorgeTsoukalas opened on Dec 30, 2025
  1

• Feature request: include the original problem descriptions in docstrings for the theorem statements

  trishullab/PutnamBench#196 · Filter by author eric-wieser opened on Aug 6, 2024
  5

• Proposal: Use sigma types with partial proofs for solution witnesses

  trishullab/PutnamBench#195 · Filter by author LasseBlaauwbroek opened on Aug 6, 2024
  5

• MathComp Analysis and idiomatic Coq formalizations

  trishullab/PutnamBench#192 · Filter by author palmskog opened on Aug 3, 2024
  7