http://grid01.ciirc.cvut.cz/~chad/cnf_todo_files.tgz

They come from a dataset of ATP problems originating from the MML (Mizar Mathematical Library). They're in CNF form and have been transformed enough that probably there are no copyright issues. Even if there are, the problems were suggested to me and given to me by the head of the relevant committee, so they're almost certainly safe to use from the copyright point of view. The 1436 problems included here are a subset of 14165 problems that seem to be hard for ATPs. (The 1436 were chosen since the 'obvious' translation of the problem would lead to too many local variables for the other problems. It took me a while to determine this since Proofgold's readdraft command reports that it had trouble normalizing the problems -- which was obviously wrong since there were no betas, etas and no definitions. There should be a clearer failure message in the case where the de Bruijn indices exceed the bound of 90.)

Each problem is a set of first order clauses. The corresponding Megalodon/Proofgold proposition asserts the set of clauses together yield False. As a small example to show how the transformation is done, suppose the set of clauses were

p(a)

-p(X) | p(f(X))

-p(f(a))

then the Megalodon/Proofgold proposition would be

forall p:set -> prop,

forall a:set,

forall f:set -> set,

(~p a -> False)

-> (forall X, p X -> ~p (f X) -> False)

-> (p (f a) -> False)

-> False

The problems have also been converted to Prover9's LADR format. If Prover9 can find a proof, it can transform it to an IVY proof. An IVY proof is detailed enough to produce a Megalodon proof and lisp code to do this is included.

If bounties are placed on these 1436 problems, then people could try to collect the bounties by running Prover9 with different options on the input file. If Prover9 finds a proof, then via IVY a Megalodon proof can be produced. Megalodon can then produce the Proofgold document to publish into the block chain and collect the bounty. This is a realistic workflow for people who would like to take part but for whatever reason do not want to directly prove propositions using Megalodon or modify another prover to produce Proofgold's Curry-Howard style proof terms.

A README in the directory has more information about what is included and how to use it.

Feedback is welcome.

]]>http://grid01.ciirc.cvut.cz/~chad/megalodon-1.7.tgz

I've added some basic automation. If you're writing a proof term to close a goal with an exact, you can write ?xx? and Megalodon will try to generate the proof term that should be in that position. If the xx is some hex characters (up to 64 hex chars, i.e., 32 bytes), then it is taken as a seed to determine random choices made during the search. If the xx is "+" or starts with "*", then Megalodon will search for an appropriate seed. The "+" option only tries the shortest 64K seeds (up to 4 hex chars). The "*" option can try more (or fewer) seeds optionally chosen by the -masl command line option, with default 64K. The "*" option can also include some hex characters as an initial seed which is then incremented if it doesn't work.

Here are a few examples:

exact ??. (This does a basic search with seed 0. Proof checking halts on failure.)

exact ?ab?. (This does a basic search given by the 32 bytes starting with byte ab with remaining bytes 0. Proof checking halts on failure.)

exact ?+?. (This tries to find a seed where at most the first two bytes are 0, admitting the subgoal if none is found.)

exact ?*ab0d25?. (This starts with the seed ab0d25000...000 and increments until a seed solving it is found, or the -masl limit is reached. Upon failure, the subgoal is admitted.)

]]>https://proofgold.org/proofgold-core-0.2.5.tgz

The changes are fairly minor. Here is a summary:

. The ltc dust limit has been updated.

. A new importwallet command has been added.

. Some changes to the networking code will hopefully make it easier for new nodes to connect and old nodes to find connections.

. The timeout for cli command calls has been removed. It often didn't work properly since it raised a Timeout exception that was often caught by the wrong thread.

http://grid01.ciirc.cvut.cz/~chad/megalodon-1.6.tgz

I updated the examples and included more about structures since these seem to be useful for the recent definitions of categories of structures.

]]>Since I'd like more participation in Proofgold, I decided to take some of the Proofgold bars I've staked over the past year and distribute them as an airdrop to addresses that held Dalilcoin fraenks in the last known Dalilcoin ledger state. (I had this information since I was running a node when it stopped producing blocks.)

There were a total of just over 70000 Dalilcoin fraenks in 1460 p2pkh and p2sh addresses. I wasn't willing to sacrifice 70000 Proofgold bars, so I divided each amount by 4 and airdropped that many Proofgold bars to the Proofgold address corresponding to the old Dalilcoin address. That's a total of just over 17500 bars airdropped by me today. The most common case was a p2pkh address holding 25 fraenks (from a staking reward). Now each of those has 6.25 bars from the airdrop.

If you held Dalilcoin and have not started running a Proofgold node, you can simply copy your old .dalilcoin/wallet file into your new .proofgold directory. If you are already running a Proofgold node, obviously DO NOT copy your old .dalilcoin/wallet file into your .proofgold directory since you will overwrite your current Proofgold wallet. For these cases I have written a new command "importwallet" that will be part of the next release (Proofgold Core 0.2.5). It can be used as follows:

importwallet /home/user/.dalilcoin/wallet

and will result in combining the current Proofgold wallet with the information in the Dalilcoin wallet. (It can also be used to combine two Proofgold wallets as well, of course.) Proofgold Core 0.2.5 should be released this weekend.

]]>And now on to Block 20000.

]]>Corresponding Megalodon and Proofgold files are available from here:

https://proofgold.org/catfilesJuly2021.tgz

A pdf report giving more details is available here:

https://proofgold.org/proofgoldcategories.pdf

I may update the report later (at the same link) to explain more or to add more conjectures.

]]>In case proofgold.org does disappear, I still plan to do what I can to help keep the peer to peer network running, so I hope people will keep running nodes and staking. The following memo.cash account should still be a way I can make announcements:

https://memo.cash/profile/1NzEUQWpb5Mze9REfkVAZ8wDcxzqpZFNJ8

]]>https://proofgold.org/proofgold-core-0.2.4.tgz

As part of the code review process I found a number of improvements than could be made. In most cases to avoid needing to document that inferior version I went ahead and made the change and documented the new version. I also made some changes that should help nodes get resynced if they get behind.

Most of the code is still undocumented. The modules config, version, zarithint, utils, json, ser, hashaux and secp256k1 have been reviewed and documented. This finishes Phases 0, 1 and 2 of the code review process suggested in January:

https://proofgold.org/forum/index.php?id=142

Here are the modules in 0.2.4 with full or partial documentation:

config https://proofgold.org/code.php?m=51

zarithint https://proofgold.org/code.php?m=52

json https://proofgold.org/code.php?m=53

version https://proofgold.org/code.php?m=54

utils https://proofgold.org/code.php?m=55

ser https://proofgold.org/code.php?m=56

secp256k1 https://proofgold.org/code.php?m=57

cryptocurr https://proofgold.org/code.php?m=58

signat https://proofgold.org/code.php?m=59

ltcrpc https://proofgold.org/code.php?m=60

script https://proofgold.org/code.php?m=61

hashaux https://proofgold.org/code.php?m=62

sha256 https://proofgold.org/code.php?m=63

ripemd160 https://proofgold.org/code.php?m=64

hash https://proofgold.org/code.php?m=65

htree https://proofgold.org/code.php?m=66

db https://proofgold.org/code.php?m=67

net https://proofgold.org/code.php?m=68

logic https://proofgold.org/code.php?m=69

mathdata https://proofgold.org/code.php?m=70

checking https://proofgold.org/code.php?m=71

assets https://proofgold.org/code.php?m=72

tx https://proofgold.org/code.php?m=73

ctre https://proofgold.org/code.php?m=74

ctregraft https://proofgold.org/code.php?m=75

block https://proofgold.org/code.php?m=76

blocktree https://proofgold.org/code.php?m=77

setconfig https://proofgold.org/code.php?m=78

commands https://proofgold.org/code.php?m=79

inputdraft https://proofgold.org/code.php?m=80

staking https://proofgold.org/code.php?m=81

proofgold https://proofgold.org/code.php?m=82

There are new options -fof and -th0 to create fof and th0 problems for ATPs whenever a proof or subproof is justified by Admitted or admit. The th0 problems contain all known results and hypotheses in context. The fof problems only contain first-order known results and hypotheses and are only generated with the conclusion is first-order. If the ATP finds a proof, it is still up to the user to inspect the ATP proof and translate it to a Megalodon proof.

I also fixed some bugs in the Dieudonne_2_2 file from Megalodon 1.4. Some of these were pointed out by Blake (thanks for proofreading!). One bug was found by E prover ( http://eprover.org ) when I was testing the new -fof option. E claimed to find proofs that should've been too difficult for it. Looking into the details it was using the (unproven) versions of 2.2.3 from Dieudonne. Let me quote (2.2.3) from Dieudonne's book:

"Any finite subset A of R has a greatest element b and a smallest element a (i.e., a <= x <= b for every x in A)."

I formalized this as two conjectures:

Theorem Dieudonne_2_2_3a: forall A c= R, finite A -> exists a :e A, forall x :e A, a <= x.

Admitted.

Theorem Dieudonne_2_2_3b: forall A c= R, finite A -> exists b :e A, forall x :e A, x <= b.

Admitted.

I think it's fair to say that these correspond to what Dieudonne wrote. However, they are clearly not what Dieudonne meant. In contexts where E had either of these as a previous result to use, it applied it with the empty set for A. That's clearly finite. And if it had a smallest or greatest element it would contradict the fact that the empty set is empty! I don't want to speak for Dieudonne, of course, but the fact that these shouldn't apply where A is empty was probably considered too obvious to be explicit about. But in formal mathematics one must be tediously explicit about everything, and this is a nice simple example showing why. Here are the corrected versions in the new Dieudonne_2_2 file:

Theorem Dieudonne_2_2_3a: forall A c= R, A <> 0 -> finite A -> exists a :e A, forall x :e A, a <= x.

Admitted.

Theorem Dieudonne_2_2_3b: forall A c= R, A <> 0 -> finite A -> exists b :e A, forall x :e A, x <= b.

Admitted.

I also included a new file Dieudonne_2_2_extra.mg based on results from E. E claims to be able to prove (2.2.13b) from (2.2.11) and (2.2.13e) from (2.2.13c). The extra file includes these two relativized results as conjectures. If someone proves the relative results and then proves (2.2.11) or (2.2.13c), then the proof of (2.2.13b) or (2.2.13e) will just be using implication elimination to combine the results.

Finally I added a new file with some results I would like to prove if I had more time. That file is IntsAndDiadRationals1.mg. There are definitions and conjectures mostly related to integers and Diadic Rationals (as Surreal Numbers). Here is a pdf version that may be more readable:

]]>In replies I'll put a list of the problems and the addresses where the bounty is.

]]>http://grid01.ciirc.cvut.cz/~chad/megalodon-1.4.tgz

Since there were some problems with the formulations of some conjectures in 1.3, I spent some time defining a "real number structure" following Dieudonne's Foundations of Modern Analysis. So now it's possible to assume one has an abstract real number structure and then make definitions/prove theorems relative to that structure. I carved out natural numbers, integers and rational numbers from such a real number structure, so now to say "the set of rational numbers is denumerable" one can say "for every real number structure Rs, the set of rational numbers Q derived from Rs is denumerable." I added a file form100_R1.mg that reformulates some of the "Top 100 Theorems" in this style.

I also went through Section 2.2 of Dieudonne's book and formulated the 17 theorems there (and a couple of little facts) as 41 conjectures. (Many "equivalence" theorems will be easier to apply if they are a sequence of separate results.) They should be relatively easy to prove, once someone gets the hang of proving in Megalodon.

I also conjectured that the quotient of a group by a normal subgroup is a group and that the canonical map is a group homomorphism. These should be easy but tedious facts to prove.

A nice thing about old math books like Dieudonne's is that with a bit of searching anyone can find a copy online for free. If you want to formally prove some of the conjectures, the informal proofs in Dieudonne's book would likely be helpful.

]]>Six of the propositions correspond to the best known bounds of R(3,7), R(4,6) and R(5,5). A bounty of (almost) 300 bars was placed on each.

R(3,7) > 22: not_TwoRamseyProp_3_7_22 : TMJKbZjgHwR1R1hCak4EgwPjmA8HNR1AzVe

R(3,7) <= 23: TwoRamseyProp_3_7_23 : TMGKH8FtpMKQL5nSjsU22A45gjtZpd5Yarm

R(4,6) > 35: not_TwoRamseyProp_4_6_35 : TMTP6yNEuLJgxabKFMpXXG2jXMmGBhXo7LG

R(4,6) <= 41: TwoRamseyProp_4_6_41 : TMGyu8j3dnjTxE99spsMGXnkEp8QU5d7ePK

R(5,5) > 42: not_TwoRamseyProp_5_5_42 : TMbu5cNHpJ8J5t435KssbZiaKf7Av2ASGBH

R(5,5) <= 48: TwoRamseyProp_5_5_48 : TMctie53cBVHdM4Dvc2CpJMCm7QGMPDGRQm

Four of the propositions correspond to open problems. A bounty of (almost) 500 bars was placed on each.

R(4,6) > 36: TwoRamseyProp_4_6_36 : TMUnmw49fNPNqFFquQctTBy16LwoDRrxTg7

R(4,6) <= 40: TwoRamseyProp_4_6_40 : TMN4q5W37NkZMoR6vedSpCh9okznLfUoQbH

R(5,5) > 43: TwoRamseyProp_5_5_43 : TMNUq5RbcM6eMfgZZQwN7xZNjZQaoV9H2Vo

R(5,5) <= 47: TwoRamseyProp_5_5_47 : TMHQLAu8LNq833psgUYemBdTPiRj2wTeAyb

The remaining ten are weaker bounds than the best known and are stated using power sets. A bounty of (almost) 100 bars was placed on each.

R(3,6) > 16: not_TwoRamseyProp_3_6_Power_4 : TMLyvZypyq14D3Q2vyHSse88YzHewwRcCDB

R(3,7) > 16: not_TwoRamseyProp_3_7_Power_4 : TMRgsDDE1r3HdbuN5FnQLLbtL4VxT2U4oxm

R(4,5) > 16: not_TwoRamseyProp_4_5_Power_4 : TMK6infbDwDHS4b8r9xmZohrD5GBwPDg9Y6

R(4,6) > 32: not_TwoRamseyProp_4_6_Power_5 : TMNEbNDi1x9cRwNgQ365q4mQrTA21mcZzpE

R(5,5) > 32: not_TwoRamseyProp_5_5_Power_5 : TMGmDYbRXrpoiZjRi312cY1fvzjX3vVcMbz

R(3,6) <= 32: TwoRamseyProp_3_6_Power_5 : TMVhEw2QbtGaDDY51t2cwuHDMUzaETWib2D

R(3,7) <= 32: TwoRamseyProp_3_7_Power_5 : TMb4eT18NCpi4ejC4ECKxNQaagNAEGTj4LA

R(4,5) <= 32: TwoRamseyProp_4_5_Power_5 : TMV3YoyvmjyjxRvvRFvzzy1SBNJiVLAPcj7

R(4,6) <= 64: TwoRamseyProp_4_6_Power_6 : TMd3rAdqu6qzfWvG6z8fctmdsnvMEex6ykJ

R(5,5) <= 64: TwoRamseyProp_5_5_Power_6 : TMFmfYexZpQQTd5iYiCqFrsY32PBd2EqPzm

not_TwoRamseyProp_3_5_13 : TMcGK8KWhfaCkgZUqXFaa4wSTBr6oTf89PQ

TwoRamseyProp_3_5_14 : TMbShW7mSiehCqEg6gfAGZXGbBLt5TA2atT

not_TwoRamseyProp_3_6_17 : TMMeqRAd9xzG4jtxa9EUaL64uqRevdds6jW

TwoRamseyProp_3_6_18 : TMbJ1MogStdKCGN3J3j1hThprkcWjA8ggEB

not_TwoRamseyProp_4_5_24 : TMXaEY6oQ7QdVZuqvs3nB3u1a3PaeREqW4b

TwoRamseyProp_4_5_25 : TMaGCJ8SmUjESVqqhCFM894vFTpNfi7Zcbo

I checked by hand today and none of the bounties distributed since the reward bounty fund started have been collected so far.

]]>There were some other suggestions he gave that haven't been followed up on yet:

1. There are many places in the code where a try is paired with an arbtrary catch-all wildcard. This is at least bad style since in principle we should know what exceptions are possible at the given try. It is also a likely way to introduce real bugs since an exception intended to be caught somewhere else is caught "early". We should also make sure all exceptions are actually caught in order to avoid the process "silently exiting".

2. It's likely that some of the recursive functions can be rewritten to be tail recursive, making them significantly more efficient.

3. Currently there's no (or almost no?) signal handling, but obviously there should be.

There's more, but I can add them when they come to mind.

As for (1) I noticed there are some exceptions defined in the code that are never raised, so these could be deleted (unless I'm missing something):

blocktree: NoReq

ctre: MissingCTreeElt InsufficientInformation FoundHashval

mathdata: UnknownSigna UnknownTerm NotKnown NonNormalTerm TermLimit BetaLimit

We should probably identify where every exception might be raised and might be caught, and especially which exceptions can escape a function or pass through a function. I don't know a quick way of doing this and there are well over 1000 functions, so doing it by hand seems unrealistic.

As for (2) there are over 300 recursively defined functions, so it will take some time to look through them and determine if they can be made tail recursive. I'm not as motivated as I'd like to be to start going through them by hand.

Hope this helps.

]]>No one has yet proven either of the Ramsey bounties from last week, so they seem hard enough for the moment. I choose two weakened versions of R(3,4) <= 9, namely R(3,4) <= 16 (using Power 4 for 16) and R(3,4) <= 32 (using Power 5 for 32).

TwoRamseyProp_3_4_Power_4 : TMa4Lc4AyMhSWuiBQmLra5Cex3wBXf15o16

TwoRamseyProp_3_4_Power_5 : TMQzy35yBcche2UXwdvoZVnt3dyp4LnFDNx

I expect these are much easier than proving R(3,4) <= 9 from last week, but by proving R(3,4) <= 9 should allow one to easily infer these two weaker versions. If no one proves a weaker version first, proving the strong version will allow someone to prove the two weaker version collect all three bounties.

The other Ramsey problems deal with R(4,4). The tight bounds correspond to R(4,4) > 17 and R(4,4) <= 18.

not_TwoRamseyProp_4_4_17 : TMFYWunQezDrkhpMUee7saZdayoEVM4SsbP

TwoRamseyProp_4_4_18 : TMbeXnozpPPnYPGE5hdooJdVvco3rwg45tS

In addition there are four weaker versions correspodning to R(4,4) > 8, R(4,4) > 16, R(4,4) <= 32 and R(4,4) <= 64.

not_TwoRamseyProp_4_4_Power_3 : TMb2Sy7PW4A7JxWuNHKhF1RyJi1ALA12yEn

not_TwoRamseyProp_4_4_Power_4 : TMV3LTHyCBnhXvur7GPWJBv9EbT5YUC4S8K

TwoRamseyProp_4_4_Power_5 : TMM1zbu3WmwYVsxxmcESD8kFqbfFQwTcR4f

TwoRamseyProp_4_4_Power_6 : TMJv5tmSnJSKJgVYvRKQVVMBttzVWdfnLJf

Finally, the third problem from the "top 100" list is denumerability of the rationals. There were 10 different formulations distributed with Megalodon 1.3, many of which are very similar, so I choose 3 representatives. When I chose them they all looked correct, but explaining them below I found problems with all three. I now think none of them are legitimate formulations of the third problem from the top 100 list, but I have already placed the three bounties so people can prove the buggy versions. Fortunately two of the three are close enough that solving them should quickly lead to a solution to a correct formulation.

form100_3_v3 : TMXKMYuE8hRapjyBpEa6rbp5tbDWKWiaANc

form100_3_v6 : TMYTquaD9W9QCyJKFi7YAX66i65SXXiAEhE

form100_3_v10 : TMTWifAgRgCavKbE1rQvQ3SqdPxQgHHhaaU

form100_3_v3 uses finite ordinals as natural numbers collected in the first infinite ordinal omega. An equivalence relation on pairs of finite ordinals is given using natural number multiplication in a way that corresponds to the equivalence of fractions. The quotient by this relation is asserted to be equipotent to omega. (Now that I am explaining this, it looks like there may be a bug since 0 is in omega. Every pair (n,0) will be equivalent to every other pair (m,0). The theorem still looks provable, though it may technically prove "the nonnegative rationals plus one point at infinity is denumerable.")

form100_3_v6 assumes one is working with an abstract notion of real numbers. The natural numbers can be carved out of the real numbers and then the rational numbers can be carved out of the reals. These rational numbers are asserted to be equipotent to the ordinal omega. (Again, now that I am explaining this, there appears to be a bug, this time more serious. In the definition carving out the rationals, x is said to be rational if there are (nonnegative) natural numbers n and m with m * x = n. Since m and n can be chosen to be 0, this will make every real appear to be rational. If I am reading this correctly, this formulation is not only wrong, but the way to collect the bounty is by proving the negation of the conjecture.)

form100_3_v10 assumes one is working with an explicit abstract notion of natural numbers N (starting at 1) and then takes the quotient of N :*: N (the set of pairs of natural numbers) by the equivalence relation on fractions. This is asserted to be equipotent to N. (This one appears to be mostly correct, though it only proves the positive rationals are denumerable.)

]]>https://proofgold.org/proofgold-core-0.2.3.tgz

1. There is an advantage to splitting assets into many smaller assets for staking. The main reason is that the staked asset will lose its age. If there are many small assets staking, then only that one loses its age while the others continue to gain age. This unfortunately incentivizes people to put many small locked assets into the ledger for staking. Since passing the initial pure burn stage of the blockchain, no one has staked with an asset smaller than 0.1 bars. The new code makes 0.1 bars a mandatory minimum for staking. This mandatory minimum will continue until Block 16000 at which time it will be raised to 1 bar, then after Block 18000 it will be raised to 10 bars and finally after Block 20000 it will be raised to 100 bars. This means no one should lock assets smaller than 0.1 for staking, and assets smaller than 100 bars should not be locked for longer than they will be allowed to stake.

2. There was a bug in the way age was calculated for previously locked assets. The "age" of post-locked (non-reward) assets was calculated as the difference between the current height and the height the asset unlocked. If such an asset is staked with (which happened sometimes, but not too often, less than 1% of the last 1000 blocks), then its new birthday would be greater than the height at with the asset unlocked. As a consequence such assets would not lose age when staked with. Even worse, this could be gamed by "locking" a new asset with a lock height 10000 blocks in the past and making it start with the maximum possible age. (No one was doing that, but I did an experiment to check that it was possible.)

I also made a third change: the maximum age for rewards and post-locked assets is now 5000 instead of 10000. The maximum age for locked non-reward assets (which age twice as fast) is still 10000. The intention is to make sure there is an incentive to lock assets for longterm staking.

Part of the soft fork happens immediately: any attempt to stake with an asset smaller than 0.1 bars will not be accepted. Since no one is doing this, it should not be visible. The modifications to the calculation of coinage for post-locked assets will begin at Block 5500, which should come within the next two weeks.

Stakers should update. If someone doesn't there is a chance they will stake a block considered invalid which will then be orphaned. This only applied to 1% of blocks in the last 1000, so it is not a huge risk.

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

]]>