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

Question

If I correctly understand the Curry-Howard isomorphism, each dependent type corresponds to a theorem for which the program implementing it is a proof. This means that any mathematical problem, for example a^n + b^n = c^n , can be somehow expressed as a type.

Now suppose I want to create a game that generates random types (theorems) and on which games should try to implement programs (proofs) of these types (theorems). Is it possible to control the complexity of these theorems? That is, a simple mode will generate trivial theorems, while a hard mode will generate much more complex theorems.

Answer 1

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

It is not so easy. No one knows if there are any one-way functions. Most people believe that there is, but evidence that, if true, is known is at least as difficult as proving P /= NP . However, there is a ray of light! People managed to build functions with the strange property that if some functions are one-way, then it should be. Thus, you can choose such a function and be sure enough that you will offer quite complex problems. Unfortunately, I believe that all known universal one-way functions are pretty unpleasant. Therefore, it will most likely be difficult for you to code them, and your users will most likely find even the simplest proofs too complex. So, from a practical point of view, you might be better off choosing something like a cryptographic hash function that is not so complete as to be truly one-sided, but which will undoubtedly be difficult to crack a person.

Answer 2

If you only generate types, most of them will be isomorphic to ⊥ . ∀ nm -> n + m ≡ m + n makes sense, but ∀ nm -> n + m ≡ n , ∀ nm -> n + m ≡ suc m , ∀ nm -> n + m ≡ 0 , ∀ nm xs -> n + m ≡ length xs and there are no others. You can try to create well-typed terms and then check, using something like Djinn, that the type of the generated term is not populated by a much simpler term. However, many of the generated terms will be either too simple or pointless garbage, even with a smart strategy . A typed setting contains fewer terms than non-typed ones, but the type of only one variable can be A , A -> A , A -> B , B -> A , A -> ... -> E , and all these type variables can be free or universal. In addition, ∀ AB -> A -> B -> B and ∀ BA -> A -> B -> B are essentially the same types, so your equality is not just αη, but something more complicated. The search space is simply too large, and I doubt that a random generator can create something truly nontrivial.

But maybe the terms of some particular form are interesting. Bakuriu in the comments of the proposed theorems represented by parametrism: you can just take Data.List.Base or Function or any other base module from the Agda standard library and get a lot of theorems out of thin air. Also check the documentation on the computational interpretation of parametricity , which gives an algorithm for deriving theorems from types in a dependent typed setting (although I don’t know how it relates to Theorems for free , and they do not give rules for data types). But I'm not sure that most of the theorems released will not be proved by simple induction. Although theorems on functions that are instances of left folds are usually more complicated than those that are examples of regular folds, this may be one criterion.

Answer 3

This falls into the interesting and complex field of proof of the lower bounds of the complexity of the proof. Firstly, it very much depends on the strength of the logical system used and what evidence it allows. A proposition can be difficult to prove in one system and easy to prove in another.

The next problem is that for a random sentence (in a sufficiently strong logical system) it is even impossible to decide whether it proves it or not (for example, the set of provable sentences in first-order logic is only recursively enumerable ). And even if we know that this is provable, a solution of complex complexity can be extremely difficult or unsolvable (if you find proof, this does not mean that it is the shortest).

It is intuitively similar to the Kolmogorov complexity : for a common line, we cannot determine which shortest program it produces.

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

For sufficiently large n, any proof of the Proof of PHP ^ n {n-1} _ (the Blue Hole Principle) requires a length of 2 ^ {\ Omega (n)}.

These slides give an overview of the theorem. This way you can generate offers using such a scheme, but it probably won't be very interesting for the game.