Reward Bounty Propositions

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.

Random HF

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.

• HF1: A first-order proposition is constructed using (some of) the first-order relations and functions from the HOHF theory.
• HF2: This is similar to HF1, except additionally an uninterpreted unary predicate and uninterpreted unary function may occur in the proposition.
• HF3: A first-order proposition is constructed using several uninterpreted constrants, a unary function, two unary predicates, a binary relation and a binary predicate. For the most part, constants of the HOHF theory are not used in this proposition.

QBF

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.

Set Constraints

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 t₁ ... t_n) or (∀ x y z w . P t₁ ... t_n → 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.

Higher-Order Unification

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 t₁ ... t_n = 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.

Untyped Combinator Unification

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].

Abstract HF Problems

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.

AIM Conjecture Related Problems

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:

• Primitive 96 [binop_on]: binop_on X f means f is a binary operator on a set X. Here f has type ι→ι→ι. That is, f is not itself encoded as a set.
• Primitive 97 [Loop]: Loop X m b s e means m, b and s are binary operations on X satisfying the loop axioms (with e as identity) (Warning: This definition has a serious bug. The condition that e is in X is missing.): m e x = x, m x e = x, m x (b x y) = y, b x (m x y) = y, m (s x y) y = x and s (m x y) y = x.
• Primitive 98 [Loop_with_defs]: Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 means Loop m b s e holds and the following defining equations hold:
  • K x y = b (m y x) (m x y))
  • a x y z = b (m x (m y z)) (m (m x y) z))
  • T x u = b x (m u x)
  • I1 x u = m x (m u (b x e))
  • J1 x u = m (m (s e x) u) x
  • I2 x u = m (b x u) (b (b x e) e)
  • J2 x u = m (s e (s e x)) (s u x))
  • L x y u = b (m y x) (m y (m x u))
  • R x y u = s (m (m u x) y) (m x y)
  Here K gives the commutator of two elements (which is the identity if the two elements commute) and a gives the associator of three elements. The remaining operators construct inner mappings given one or two parameters. A loop is an AIM loop if all inner mappings commute.

If the AIM conjecture is true, the following two identities must hold in all AIM loops:

• K (m (b (L x y u) e) u) w = e
• a w (m (s e u) (R x y u)) z = e
The next two primitives are predicate recognizing loops with a counterexample to one of these identities.
• Primitive 99 [Loop_with_defs_cex1]: Loop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2 means Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 holds and there exist elements u, x, y and w of X such that K (m (b (L x y u) e) u) w ≠ e.
• Primitive 100 [Loop_with_defs_cex2]: Loop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2 means Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 holds and there exist elements u, x, y, z and w of X such that a w (m (s e u) (R x y u)) z ≠ e

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.

Diophantine Problems

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 2⁶⁰.

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:

• Primitive 9 [Empty] : The empty set has cardinality 0.
• Primitive 11 [Power] : Power X has cardinality 2ⁿ if X has cardinality n.
• Primitive 71 [binrep] : binrep X Y has cardinality m + 2^{n if X and Y have cardinality m and n, respectively.}

Addition and multiplication correspond to disjunction unions and products of sets:

• Primitive 68 [setsum] : setsum X Y has cardinality m + n if X and Y have cardinality m and n, respectively.
• Primitive 73 [setprod] : setprod X Y has cardinality m * n if X and Y have cardinality m and n, respectively.

Instead of the ≤ relation, we use the existence of an injection:

• Primitive 51 [inj]: inj X Y f means f is an injection from X into Y.
• Primitive 53 [atleastp]: atleastp X Y means there is an injection from X into Y.

Instead of equality, we use equipotence:

• Primitive 52 [bij]: bij X Y f means f is a bijection from X into Y.
• Primitive 54 [equip]: equip X Y means there is a bijection from X into Y.

For equality modulo a number, we use the following:

• Primitive 103 [equip_mod] : equip_mod X Y M means there exist sets Z and V such that either equip (setsum X Z) Y and equip (setprod V Z) M or equip (setsum Y Z) X and equip (setprod V Z) M. Intuitively, Z is the difference of X and Y and V witness that this difference divides the modulus.