Second Proposal for Reward Bounties

by Brown, Tuesday, October 27, 2020, 13:08 (404 days ago) @

With the HOL4 dataset there were a few problems that were too big, and I've already filtered those out. In general I omitted a problem if its description in a Proofgold document exceeded 200K bytes. Most take significantly less size than that. Generally speaking the Mizar documents are much smaller than the HOL4 ones, presumably because of all the "ap" and "lam" occurrences in the HOL4 ones. I also filtered out some other problems for various reasons (too easy or duplicates of other problems).

The problems don't need to be published into the Proofgold blockchain except when needed. I suspect this will happen when someone proves the theorem. If so, they'll be published at a slow enough rate to be reasonable. To know where to put the automatic bounties, we only need to know the address (20 bytes) of each candidate proposition. I made another post with the code containing a big array of the addresses, and it seems reasonable.

In your other post you mentioned coqhammer and sledgehammer. Are you thinking maybe some problems that originate from Coq or Isabelle should be included? If so, can you suggest a way to get a collection of relevant problems?