Proposal: Use sigma types with partial proofs for solution witnesses

[LasseBlaauwbroek]

I wonder if the current structure of formalizations where an answer must be synthesized is the best.

Instead of having a 'solution' definition that needs to be filled in, wouldn't it be more convenient if it were encoded with a sigma type? Then, for contestants who cannot synthesize the answer, the witness can be pre-chosen by filling in part of the proof:

Theorem putnam_1963_b1 : { P : int -> Prop | forall (R : realType) (a : int), 
  (('X^2 - 'X + a%:~R) : {poly R}) %| ('X^13 + 'X + 90) <-> P a }.
Proof.
exists (fun i : int => i = 2).
Admitted.

Instead of:

Definition putnam_1963_b1_solution (i : int) : Prop := i = 2.
Theorem putnam_1963_b1 (R : realType) (a : int) :
 (('X^2 - 'X + a%:~R) : {poly R}) %| ('X^13 + 'X + 90) <-> putnam_1963_b1_solution a.

In addition to this solution feeling more natural, it also makes things more consistent: The problem discussed in #183 also has a sigma type that finds a certain bound. Although the text description doesn't make it explicit, this sigma type must still be synthesized with a concrete number. (Unless there is some crazy situation where it can be proven non-constructively, but that seems unlikely.)

Many of the definitional witnesses also do not seem correct, especially the ones that concern propositions:

PutnamBench/coq/src/putnam_1988_b2.v

Lines 3 to 6 in cca47f7

	Definition putnam_1988_b2_solution := True.
	Theorem putnam_1988_b2
	: (forall (a: R), a >= 0 -> forall (x: R), pow (x + 1) 2 >= a * (a + 1) ->
	pow x 2 >= a * (a - 1)) <-> putnam_1988_b2_solution.

If I'm allowed to fill in this solution myself, I can easily prove the theorem by just making the solution a copy of the theorem. Instead, it should again be encoded as a sigma type:

Require Import Reals Coquelicot.Coquelicot.
Open Scope R.

Definition decidable P := {P} + {~P}.

Theorem putnam_1988_b2 : decidable 
  (forall (a: R), a >= 0 -> forall (x: R), pow (x + 1) 2 >= a * (a + 1) ->
    pow x 2 >= a * (a - 1)).
Proof.
left.
Admitted.

I would propose the same thing for Lean.

[eric-wieser]

Instead of having a 'solution' definition that needs to be filled in, wouldn't it be more convenient if it were encoded with a sigma type?

I think this is problematic, since the sigma type can then just be populated with the axiom of choice, and you can no longer inspect the statement alone to check what answer was given.

[LasseBlaauwbroek]

As long as the sigma types are in the computationally relevant realm I don't see the problem. In Coq, you would need to import some pretty controversial axioms to 'cheat' your way through things. (And axioms will have to be checked anyway.)

In lean, you would have to mark a definition as noncomputable in order to use choice. So it should be safe. The pattern could look something like this:

def test : Decidable True :=
  Decidable.isTrue (by sorry)

[LasseBlaauwbroek]

Looking at this again, I realize that my original proof statement of 1963/b1 was wrong:

Theorem putnam_1963_b1 : { P : int -> Prop | forall (R : realType) (a : int), 
  (('X^2 - 'X + a%:~R) : {poly R}) %| ('X^13 + 'X + 90) <-> P a }.
Proof.
exists (fun i : int => i = 2).
Admitted.

In fact, this theorem is trivial to prove by just instantiating the existential quantifier to fun a => (('X^2 - 'X + a%:~R) : {poly R}) %| ('X^13 + 'X + 90). This is because the statement asks for a non-computational witness P : int -> Prop. Instead, it should be a computational witness P : int -> bool.,,

The tricky thing here is that the informal statement asks to 'find all integers for which...'. It is not even quite clear what this means. If there are finitely many such integers, finding them might entail providing a list. If there are infinitely many, it should rather be a function int -> bool.

Creating formal abstracts is hard!

[eric-wieser]

This is because the statement asks for a non-computational witness P : int -> Prop. Instead, it should be a computational witness P : int -> bool.

In Lean, many such witnesses are impossible; there is no computable witness for "real numbers that are even integers" (as AlphaProof used in IMO 2024 P1), because equality of real numbers is not decidable in Lean. I would imagine even in Coq, there are some closed-form answers which would be accepted by a Putnam examiner, but would not in fact be computable.

[LasseBlaauwbroek]

Yes, you are right. Problems like IMO 2024 P1 are inherently ambiguous, just like problems that ask to simplify an expression are ambiguous. I don't think there is any reasonable way to encode problems of the form 'determine all real numbers such that...'. If the set is finite you can use a list. If the set is countable, maybe you can use a coinductive list. But if the set is uncountable, the answer is ambiguous.