TMZPAPyEPS2GSQjei1QuePMKCa7TyyrZ5LW: t6_cat_3 t7_cat_3

TMHf56pApyotpY8gCP4bupxVi8DUpVHhmci: t8_complex2 t9_complex2

TMYojCRLszJwjbrkaAkLcncph364s5kmzbJ: t80_transgeo t51_transgeo

TMXeAgzusRtUTzsYk3AdMwsBvZ8ctA1FsET: t48_transgeo t75_transgeo

TMRXVZNXJVHJmuCnpoyvfY5hUPG8PZ9cJLp: t49_sin_cos3 t47_sin_cos3

TMZUqc5UpZHn6b2goxw31ZE6HtEKzdh2EYb: t47_yellow_4 t20_yellow_4

TMQco5oyqUAmmJMfsUmVPeWQusKwbwovorW: t25_tex_4 t26_tex_4

TMJBwMsMMNr2Svj6GbTq3jFce1E7H9mqmuE: t42_tdlat_1 t43_tdlat_1 t39_tdlat_1 t40_tdlat_1

This weekend I used the bounty fund to place a bounty of (almost) 25 bars on each of these 1436 problems. For people who want to solve some of them, I'd suggest downloading the .tgz file in the OP and trying to use Prover9 and the distributed lisp files to obtain a Megalodon proof and then use Megalodon to obtain a Proofgold proof.

There are roughly 3800 blocks remaining during the phase where 25 bars of the reward goes into the bounty fund. More suggestions for problems to place bounties on are welcome.

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

]]>"You don't have permission to access /~chad/megalodon-1.6.tgz on this server."

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

]]>I have an idea why nodes might have trouble connecting and have a potential fix ready for the next release.

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

]]>