Megalodon 1.8 (23257 "Conjectures")

by Brown, Saturday, November 27, 2021, 11:57 (8 days ago) @ Brown

I also meant to mention the file Nov2021ConjsAll.mg distributed with Megalodon 1.8. This file contains 23257 unproven "conjectures." I expect the vast majority of them are easy to prove or disprove, so they might make good candidates for small bounties for people just starting out trying to prove theorems and collect bounties.

They are all derived from the construction of the real numbers (and complex numbers) via the Conway surreal numbers. Here's roughly how:

At each "important" point in a proof (a cut in a sequent calculus derivation), the proof is a proof of a proposition C under n assumptions A1, ..., An. I created the conjectures by dropping one of the n assumptions (obtaining n conjectures for that step).

Dropping an assumption may make the proposition unprovable, and I expect in most cases the negation (of the global proposition) will be provable. In some cases the dropped assumption isn't really needed (or is implied by the other assumptions anyway) so the proposition is still provable.