Four of the propositions correspond to four of the "top 100 theorems" from here:

http://www.cs.ru.nl/~freek/100/

The formulations used were the first formulations distributed with Megalodon 1.3. All four formulations are properties of the natural numbers as represented by the ordinal omega.

1. TMSGYLL23o9XEp6iYQDAQqQ9Z34aNdoziFu (form100_1_v1) "The square root of 2 is irrational." The formulation used says that for all positive n and m in omega, n * n is not 2 * m * m.

11. TMVZHF69RvDmaXgNo8jCcK9ogsxiX5Lu9wE (form100_11_v1) "Infinitude of Primes" The formulation says the set of primes in omega is infinite. Here, infinite is defined to be the negation of finite. A set is defined to be finite if it is equipotent to (in bijection with) a member of omega.

19. TMMjpZ2LC1gqEKzrVpXLaGTkybfJj1JEVcL (form100_19_v1) "Four Squares Theorem" Every member of omega can be written as the sum of four squares of members of omega. The formulation here represents squares by multiplying a number by itself rather than defining exponentiation and raising the number to the power of 2. A second formulation (form100_19_v2) uses the exponent, but it looks to me like the second version follows trivially from the first, so I only used the first one.

20. TMZTvo8fggT8Ltn1GB9xcLpBtrp7iaWPETY (form100_20_v1) "All Primes (1 mod 4) Equal Sum of Two Squares" Every prime in omega that is equivalent to 1 modulo 4 can be written as the square of two members of omega.

The other two problems are Ramsey problems as described in Brown's post and linked pdf. Brown's pdf describes proofs of corresponding problems for 3-cliques and 3-anticliques, and formal proofs for those cases were in Megalodon 1.3. I generally think this is a good policy when suggesting problems for bounties: formulate them precisely (in Megalodon, Proofgold or something else), formulate a simpler version, prove the simpler version and write an informal description. I won't demand this and welcome all suggestions, but it definitely helped in this case.

TMZTRwksZ429x7jwcuaATRxKhUvGEdp5Nyj (not_TwoRamseyProp_3_4_8) There is a symmetric edge relation (giving a graph on the ordinal 8) where there are no cliques of size 3 and no anticliques of size 8.

TMNqnATDwgaDsTFX1M9RmSouPYDn9u67dAZ (TwoRamseyProp_3_4_9) Every symmetric edge relation on the ordinal 9 has either a clique of size 3 or an anticlique of size 4.

]]>