Is it possible to randomly generate theorems that are arbitrarily difficult to prove?

Question

If I understand Curry-Howard's isomorphism correctly, every dependent type correspond to a theorem, for which a program implementing it is a proof. That means that any mathematical problem, such as a^n + b^n = c^n can be, somehow, expressed as a type.

Now, suppose I want to design a game which generates random types (theorems), and on which plays must try to implement programs (proofs) of those types (theorems). Is it possible to have control over the difficulty of those theorems? I.e., an easy mode would generate trivial theorems while a hard mode would generate much harder theorems.

Answer 1

A one-way function is a function that can be calculated in polynomial time, but that does not have a right inverse that can be calculated in polynomial time. If f is a one-way function, then you can choose an argument x whose size is determined by the difficulty setting, calculate y = f x, and ask the user to prove, constructively, that y is in the image of f.

This is not terribly simple. No one knows whether there are any one-way functions. Most people believe there are, but proving that, if true, is known to be at least as hard as proving P /= NP. However, there is a ray of light! People have managed to construct functions with the strange property that if any functions are one-way, then these must be. So you could choose such a function and be pretty confident you'll be offering sufficiently hard problems. Unfortunately, I believe all known universal one-way functions are pretty nasty. So you will likely find it hard to code them, and your users will likely find even the easiest proofs too difficult. So from a practical standpoint, you might be better off choosing something like a cryptographic hash function that's not as thoroughly likely to be truly one-way but that's sure to be hard for a human to crack.

Answer 2

If you generate just types, most of them will be isomorphic to ⊥. ∀ n m -> n + m ≡ m + n is meaningful, but ∀ n m -> n + m ≡ n, ∀ n m -> n + m ≡ suc m, ∀ n m -> n + m ≡ 0, ∀ n m xs -> n + m ≡ length xs and zillions of others are not. You can try to generate well-typed terms and then check, using something like Djinn, that the type of a generated term is not inhabited by a much simpler term. However many generated terms will be either too simple or just senseless garbage even with a clever strategy. Typed setting contains less terms than non-typed, but a type of just one variable can be A, A -> A, A -> B, B -> A, A -> ... -> E and all these type variables can be free or universally quantified. Besides, ∀ A B -> A -> B -> B and ∀ B A -> A -> B -> B are essentially the same types, so your equality is not just αη, but something more complex. The search space is just too big and I doubt a random generator can produce something really non-trivial.

But maybe terms of some specific form can be interesting. Bakuriu in comments suggested theorems provided by parametricity: you can simply take Data.List.Base or Function or any other basic module from Agda standard library and generate many theorems out of thin air. Check also the A computational interpretation of parametricity paper which gives an algorithm for deriving theorems from types in a dependently typed setting (though, I don't know how it's related to Theorems for free and they don't give the rules for data types). But I'm not sure that most produced theorems won't be provable by straightforward induction. Though, theorems about functions that are instances of left folds are usually harder than about those which are instances of right folds — that can be one criteria.

Answer 3

This falls into an interesting and difficult field of proving lower bounds in proof complexity. First, it very much depends on the strenght of the logic system you're using, and what proofs it allows. A proposition can be hard to prove in one system and easy to prove in another.

Next problem is that for a random proposition (in a reasonably strong logic system) it's even impossible to decide if it's provable or not (for example the set of provable propositions in first-order logic is only recursively enumerable). And even if we know it's provable, deciding its proof complexity can be extremely hard or undecidable (if you find a proof, it doesn't mean it's the shortest one).

Intuitively it seems similar to Kolmogorov complexity: For a general string we can't tell what's the shortest program that produces it.

For some proof systems and specific types of formulas there are known lower bounds. Haken proved in 1989:

For a sufficiently large n, any Resolution proof of PHP^n{n-1}_ (Pigeon hole principle) requires length 2^{\Omega(n)}.

These slides give an overview of the theorem. So you could generate propositions using such a schema, but that'd probably won't be very interesting for a game.