I'm neither a mathematician nor too familiar with Metamath (more of a crank really), but I'm wondering whether it is possible to build a program that automatically checks and financially rewards proofs of theorems not yet contained in the set.mm database, say the ones from the Metamath 100 list. Seeing the OpenAI work made me interested in this again.
The main problems I see are: 1. Definitions vs. axioms. The proof either (1.1) must not contain $a statements, to avoid directly or indirectly proving the end result with spurious assumptions, or (1.2) $a statements must somehow be restricted to those that only allow syntactic rewriting, without changing any semantics. I'm not sure if this is possible, or if this has been done before. 2. Since no new assumptions can be introduced, I'm not sure if all axioms contained in set.mm suffice to allow the formulation of all the remaining proofs in the MM100, or say, even cutting edge research. Is this known? Do current mathematical researchers know for certain that their assumptions are restricted to ZFC? 3. Vast proof lengths, especially with proofs involving arithmetic. A while ago I graphed the full proof dependency graph of 2p2e4: https://twitter.com/dd4ta/status/1050433711416721408 and it was pretty big :) and created plots of the number of proof steps vs the number of theorems a proof depended on, see the readme here: https://github.com/void4/mmplot Could you estimate where "cutting edge" mathematical research would be? Millions of proof steps and tens of thousands of dependencies? - Arndt -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6146e5a7-255f-4e36-86c9-feb34e50fd2cn%40googlegroups.com.
