Second Proposal for Reward Bounties

by Brown, Wednesday, October 28, 2020, 15:01 (403 days ago) @

Thanks for the pointer to the coqhammer code. I'll look into using it, but unless it's very easy to produce some problems I probably won't. It was easy with the Mizar and HOL4 problems because most of the work was already done and the problem sets have been around (and debugged) for a while.

I remember now that one of the main Isabelle developers is very anticrypto. (While I know this for sure from a personal conversation with him last year, he has also made public anticrypto talks with slides available online, so it's not really a secret or insider information.) Out of respect for his views and to avoid pointless controversy I'd recommend steering clear of Isabelle problems altogether.