Examples of Publishing Documents and Collecting Bounties

by Brown, Saturday, June 27, 2020, 17:43 (526 days ago)

I'm working on ways to produce Proofgold documents with proofs of conjectures with bounties, but thought it would be good to show that it can be done by hand already.

I've published a few documents and will describe three below. Two of the documents resolved reward bounty conjectures and so I was able to collect the 25 bar bounties for each of these. Here's a high level description first:

The conjecture for Block 128 was in the "Random2" class. It's easy to see it's not provable and that the negation is provable. Here is the negation of the conjecture in two formats:

https://proofgold.org/bountyasm/neg_a7283e160928c772524d03742845eae53562b68550237820416...

https://proofgold.org/bountythf/thf_neg_a7283e160928c772524d03742845eae53562b6855023782...

Looking at it abstractly, the (positive) conjecture says:

For every predicate P and every function F, Q and not P(F(F(t))

where Q is some big proposition involving P and F, and t is some term.

It's easy to prove the negation by assuming the proposition is true and instantiating P with the constantly True predicate. Then we get "not True" as a consequence and a contradiction follows. I'll pure more details and a link to the source document in a reply below.

The conjecture for Block 171 was in the AbstrHF class. Here is the fof+ version:

https://proofgold.org/bountyfof/fof_pos_8b6487a6e60f70caa643209c149dc82110e6de69b0afe29...

The ATP E (eprover.org) could easily prove this. Translating from an E proof to a Proofgold proof in general would require some work, but in this case inspecting E's proof made it obvious that only one axiom was needed to prove the conjecture. With some help from ocaml code I could print out a proof term Proofgold accepted. More details are in a reply below.