I guess the "fundamental theorem of automation" is that things are worth automating in proportion to both how repetitive and how simple they are. So this does sound like something that wouldn't happen that often and is relatively complex.
However one thing I would love to see is formal statements of theorems people would like to be proven. I struggle to even formalise the statement of the theorem so having some which are already stated to have a go at would suit me well. So yeah if you wanted to influence the development of the system laying down a statement yourself and then offering a cash prize might motivate people in that direction. On Thursday, September 24, 2020 at 10:04:19 AM UTC+1 [email protected] wrote: > On Wed, Sep 23, 2020 at 11:41 PM [email protected] > <[email protected]> wrote: > > 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? > > The 100 theorems on that list should all be consequences of ZFC. Only > fairly specialized mathematics needs stronger axioms than ZFC. I don't > know how certain you want, but as far as I know stronger axioms are > pretty rare, with the possible exception of the Continuum Hypothesis. > > -- > The standard is written in English . If you have trouble understanding > a particular section, read it again and again and again . . . Sit up > straight. Eat your vegetables. Do not mumble. -- _Pascal_, ISO 7185 > (1991) > -- 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/65443868-d971-40f9-aefe-bf40251487ebn%40googlegroups.com.
