Until Block 5000 half of each block reward was placed as a bounty on a proposition. The proposition was pseudorandomly determined from a seed determined by the litecoin transaction id of the previous burn transaction and the litecoin block id in which that transaction was confirmed. All the propositions are within the HOHF theory of hereditarily finite sets described here.
A collection of the first ten reward bounty propositions (determined by the first ten Proofgold blocks) in different formats is available here
The propositions fall into twelve classes which we group into eight sections below. In some cases the attempt to construct a propositon may fail. In that case, the last class (Diophantine problems) are used as a fallback.
There are three clases of random propositions related to hereditarily finite. The propositions in this class are all first-order, although higher-order axioms of the theory may be required to construct a proof.
A QBF (quantified boolean formula) proposition is created starting with a quantifier prefix of between 50 and 55 quantifiers followed by an equivalence between two propositions using all the quantified variables. The two propositions are constructed using equivalence, implication, negation and false.
A set constraint problem asserts that there are not four predicates (of types like ι → ... ι → o) satisfying eight set constraints. A set constraint for a predicate variable P has a form like (∀ x y z w . s → P t1 ... tn) or (∀ x y z w . P t1 ... tn → s).
If there is a solution to the set constraint problem the negation of the proposition can be proven by assuming there is no solution and then using the solution to prove a contradiction.
A higher-order unification problem is a proposition stating there is no solution for four higher-order variables satisfying eight flex-rigid pairs. A flex-rigid pair is of the form (∀ x y z w . F t1 ... tn = s) where F is one of the variables to solve for and the head of s is not one of the variables to solve for.
If there is a solution to the unification problem the negation of the proposition can be proven by assuming there is no solution and then using the solution to prove a contradiction.
An untyped combinator unification problem is a proposition saying there are not four combinators satisfying eight flex-rigid pairs. HF sets are used to represent (untyped) combinators. Specific (distinct) sets are used to represent the combinator S, the combinator K, and the application of two combinators. The predicate recognizing combinators is built into the HOHF theory using defined primitive 101 [combinator]. The equivalence relation given by S and K reduction is built into the HOHF theory using defined primitive 102 [combinator_equiv].
A collection of 1229 specific first-order propositions are in the array ahfprops in checking.ml. These are within a context of 24 constants, functions, predicates and relations (see ahfctx in checking.ml). If the 24 variables in context are fixed to be certain values in HOHF, then the propositions are true statements. That is, each proposition is the abstract version of a concrete first-order theorem of HOHF.
An abstract HF Problem chooses one of the 1229 as a conclusion and selects roughly 76 of the remaining 1228 as premises and forms the proposition asserting the conclusion follows from the premises. To be more precise each of the other 1228 propositions has a 1 in 16 chance of being included as a premise.
Two classes of problems are related to the AIM Conjecture, an open problem in mathematics. To support these propositions the following primitives are built into the HOHF theory:
If the AIM conjecture is true, the following two identities must hold in all AIM loops:
The two classes of AIM propositions for reward bounties are based on the two kinds of counterexample types. In each case the proposition says that every loop for which some collection of inner mappings commute and (possibly) some collection of inner mappings have a small order (dividing 2, 3, 4 or 5) does not have one of the two types of counterexamples. To be more precise, the proposition says that False follows from the assumption Loop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2 or Loop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2 and the extra assumptions that some inner mappings commute and some inner mappings have small orders.
The propositions are (generally) not equivalent to the AIM conjecture. The assumption that some inner mappings commute will not generally imply all inner mappings commute, allowing for non-AIM loops as counterexamples (to prove negated propositions). Likewise not all AIM loops will satisfy the extra conditions that certain inner mappings have a small order, so in some cases these extra conditions will allow us to prove the proposition without proving the AIM Conjecture itself.
The final two classes of problems are inspired by Diophantine equations (see Hilbert's tenth problem). In each case two polynomials in three unknowns x, y and z are generated. The exponents range from 0 to 3, so that there are (at most) 64 monomials in each polynomial. The coefficent for each monomial ranges from 0 to 15.
The class of Diophantine-Modulo problems includes propositions that state there is no solution to the equation p + 16 = q modulo m where p and q are polynomials as described above and m is a number between 2 and 260.
The class of Diophantine problems includes propositions that state there is no solution to the equation p + 16 = q or inequality p + 16 ≤ q.
Technically, integers are not used to formulate these propositions, but cardinality of sets. Specific numbers are represented as sets known to have the corresponding cardinality. The construction of such sets is supported by the following primitives of the theory:
Addition and multiplication correspond to disjunction unions and products of sets:
Instead of the ≤ relation, we use the existence of an injection:
Instead of equality, we use equipotence:
For equality modulo a number, we use the following: