Mizar CNF Problems and Prover9 Proofs

by BlakeKeiller, Sunday, September 05, 2021, 20:17 (91 days ago) @ Brown

I've downloaded it and had a quick look. I'll consider it. It's good timing in two ways: First, it's been roughly 1500 blocks since the last time I distributed bounty fund rewards, so it would be easy to put roughly 25 bars as a bounty on this many problems. Second, I had already prepared more Category Theory problems and was planning to distribute bounties to those today (after spending the weekend publishing the corresponding documents). I'd really rather give preference to problems chosen by someone else. I want to spend more time looking at the Mizar CNF dataset before deciding for sure though. I'll post here if I have questions or find potential issues.