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

[yuanyehome]

Hi,
I've noticed that there is a "no answer" option in the leaderboard (https://trishullab.github.io/PutnamBench/leaderboard.html) and no submissions are shown. What's the meaning of this leaderboard?

[GeorgeTsoukalas]

Hi! Roughly half the Putnam problems are phrased in the form of a question:

"Is it true that XYZ?"

The way we support a formalization of this in Lean is by having a secondary solution definition, where the solver is required to give a value for it. Here is an example:
(/lean4/src/putnam_2010_b1.lean)[https://github.com/trishullab/PutnamBench/blob/b391f48b645c5b6101ed89aca96230226d654b3e/lean4/src/putnam_2010_b1.lean#L5]

Alternatively, the solver can use the correct answer (but still has to prove the problem!) by writing in the value in comments below the definition. This is the approach everybody has submitted with in the leaderboard. The no answer option requires the solver to "choose" the answer as well. This makes the problem harder generally, but also less clear how to grade. In the example above, you would think "True" or "False" are valid choices, but so is "(∃ a : ℕ → ℝ, ∀ m : ℕ, m > 0 → ∑' i : ℕ, (a i)^m = m)", which is a Prop, but doesn't solve the problem (and the proof also becomes trivial with this answer). In the case of Prop types, perhaps True/False should be the only allowable answers. But definitions can have other types and what is an acceptable solution is less clear. (That's why I think nobody has submitted no-answer approaches to the leaderboard).

[yuanyehome]

Thanks for your detailed explanation! That's very clear and helpful!