Examples of Publishing Documents and Collecting Bounties

by Brown, Saturday, June 27, 2020, 18:26 (526 days ago) @ Brown

Lastly, here is the text source of the document proving the conjecture from Block 171:

https://pastebin.com/xx4QuJmt

This document isn't particularly readable. The theorem itself could have been copied from here:

https://proofgold.org/bountyasm/pos_8b6487a6e60f70caa643209c149dc82110e6de69b0afe29d662...

It looks like I reprinted it with my own code though, since the let abbreviations for "not" and "or" are not used in my version.

The theorem has the form

forall ..., Hyp1 -> Hyp2 -> ... -> Hyp73 -> Concl

Only one of the Hyps is used (as became evident from the E proof). As a consequence the proof term simply looks like a sequence of 73 lambda abstractions only one of which needs to be given an explicit name, and then this one hypothesis being used in a fairly trivial way:

TmLa ...
PrLa _ ... ...
PrLa A1 All x32 set Imp Ap Ap x2 x32 Ap Ap x11 Ap x10 x5 Ap x10 Ap x10 x5 Imp Ap Ap x1 Ap x10 x5 x32 Ap Ap Prim 5 Ap Ap Prim 5 Ap Ap Prim 5 Eq set x32 x4 Eq set x32 Ap x10 x5 Eq set x32 Ap x10 Ap x10 x5 Eq set x32 Ap Ap x11 Ap x10 x5 Ap x10 Ap x10 x5
PrLa _ ... ...
TmLa x21 set PrLa A2 Ap Ap x2 x21 Ap Ap x11 Ap x10 x5 Ap x10 Ap x10 x5 PrLa A3 Ap Ap x1 Ap x10 x5 x21 PrLa _ Ap Ap x1 x5 x21
PrAp PrAp TmAp A1 x21 A2 A3

After getting the right format and checking it with readdraft, I published it the same way as Pfg128: addnonce, addpublisher, commitdraft, publishdraft. Then I collected the bounty with collectbounties.

I hope this information is useful. When I have the first reasonable tool/tools for producing documents without doing everything by hand, I'll make a post about it.