New Bounties

by BlakeKeiller, Sunday, January 10, 2021, 12:32 (329 days ago)
edited by BlakeKeiller, Sunday, January 10, 2021, 12:35

I've now distributed 11 more bounties from the reward bounty fund. Each bounty is almost 375 bars (a little less due to transaction fees). 8 of the propositions are Ramsey Problems and 3 are 3 different (buggy) versions of the third "top 100" theorem.

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