Putnam 2017 B2 issues

[LasseBlaauwbroek]

Another one from the paper:

PutnamBench/coq/src/putnam_2017_b2.v

Lines 3 to 11 in 6ddcaac

	Theorem putnam_2017_b2
	(mina : nat)
	(posMin : mina > 0)
	(A : nat -> nat -> nat := fun a k => Z.to_nat (floor (sum_n (fun i => Raxioms.INR (a + (i + 1))) k)))
	(p : nat -> nat -> Prop := fun N k => exists (a: nat), a > 0 /\ A a k = N)
	(q : nat -> Prop := fun N => p N 2017 /\ forall (k: nat), k > 1 -> k <> 2017 -> ~ p N k)
	(hmina : q (A mina 2017))
	(hminalb : (forall (a: nat), a > 0 /\ q (A a 2017) -> mina <= a))
	: mina = putnam_2017_b2_solution.

• Why does a problem related only to natural numbers involve real numbers? Seems convoluted and makes proving it more difficult.
• The way the theorem is stated seems very awkward. It says: "If you give me a number for which you can prove the requirement from the problem, then that number must be 16." I would expect more something much more straightforward like "the number 16 has the required properties":

Require Import Nat ZArith Reals.
Definition putnam_2017_b2_solution := 16.
Theorem putnam_2017_b2 :
  let seq a k := sum_nat a (a + k - 1) in
  let valid a := a > 0 /\ forall b k, b > 0 -> k > 1 -> seq a 2017 = seq b k -> k = 2017 in
  valid putnam_2017_b2_solution /\ forall a, valid a -> putnam_2017_b2_solution <= a.
Proof. Admitted.

Not only is this simpler, but the difference really matters. You can prove the original statement assuming this new statement, but not the other way around...

I'm seeing these kinds of patterns happen in other problems as well. My guess is that this happens because of the desire to inline all 'definitions' into the theorem. Why do this? Is there a problem with separate definitions?

[GeorgeTsoukalas]

Thanks for pointing this out!

Why does a problem related only to natural numbers involve real numbers? Seems convoluted and makes proving it more difficult.

At the time, our understanding was that sum_n only allowed summands which came from a type which abelian group structure. Summing over ints also led to problems, which was probably due to insufficient imports. In some formalizations which rely on Coquelicot's sum_n, we have modified to summand to be of type real. Anyways, these occurrences will change as we complete the migration to Mathcomp.

The way the theorem is stated seems very awkward. It says: "If you give me a number for which you can prove the requirement from the problem, then that number must be 16." I would expect more something much more straightforward like "the number 16 has the required properties":

I tend to agree that this one does seem to be a bit awkwardly stated. At least for Lean + Isabelle, I think the goals are generally stated in a way that matches the one you've proposed. As we go through the modifications for the Coq problems, we should clear up any of these.

I'm seeing these kinds of patterns happen in other problems as well. My guess is that this happens because of the desire to inline all 'definitions' into the theorem. Why do this? Is there a problem with separate definitions?

The formalizations are meant to be self-contained inside the theorem statement as is consistent with other competition math benchmarks we've seen. Also, our internal tooling happens to work best in this form, as does most of the other public tooling we are aware of.

[GeorgeTsoukalas]

I have included a mathcomp-based formulation of your suggestion in #201. There is also an analogous change for the Lean problem, which was stated in the same way. The original formalization of this problem was probably somewhat awkward because it was among the first problems we started with. As the modifications for Coq continue, any other similar issues should clear up. Thanks again!

[LasseBlaauwbroek]

Why is there all this casting between integers and naturals going on? Seems to me that the problem can be entirely stated using natural numbers. The way it is written now makes it seem like there is something special going on.

Also, inconsistent usage between > and gt.

[LasseBlaauwbroek]

Also, for the Lean version, why not use let just like in Coq? These versions where a variable is hypothesized with an equality that defines the behavior of the variable are quite difficult to read.

[GeorgeTsoukalas]

Why is there all this casting between integers and naturals going on? Seems to me that the problem can be entirely stated using natural numbers.

From experience in proving stuff in Lean, it's easier to reason about sums over integers than nats as one is allowed all the ring operations. As an example, putnam_1988_b1 is much more annoying to prove if the statement is entirely in nats.

Also, inconsistent usage between > and gt.

The > operator does not work for nats when ring_scope is opened. gt is an operation defined for nats, and does not work immediately for ints.

These versions where a variable is hypothesized with an equality that defines the behavior of the variable are quite difficult to read.

I agree that the way this is done right now is a bit cumbersome to parse. We will eventually find a better way to state these things, maybe with some new syntactic shortcuts we request of the Lean community, or as you suggest. For now, this is a somewhat lower priority task.