In the programming community there is a nice tradition to solve programming puzzles on each day of advent, the most famous such challenge being Advent of Code. I have not been patient enough to create enough Metamath puzzles and, needless to say, advent has already started, yet I propose something similar: the Metamath Christmas challenge! The goal is to prove a small but remarkable theorem of Ryley, that every rational number is a sum of three cubes of rational numbers:
* $d a b c A $. 3cubes $p |- ( A e. QQ <-> E. a e. QQ E. b e. QQ E. c e. QQ A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) ) $= ? $.* To ease the task, I prepared a file with four lemmata, which should help you fill in the gaps and finish the proof: https://gist.github.com/savask/953a9c38205fb714607faec80ac57b7b Notice that I have not formalized the proof myself, so if you see a problem with the file, please tell me, and I will hopefully fix it. I hope someone will find this little challenge interesting - of course, the first person to formalize the proof has the full rights to put their name on the theorem and claim it for themselves :-) *Related questions* 1. When preparing the challenge, I was wondering if I missed a bracket somewhere or forgot to put some brackets etc. Is there an easy way to check that a statement passes grammar checks? I think mmj2 could do that, but it is rather cumbersome to use as it is not really supported anymore. 2. In 2017 Norman suggested <https://groups.google.com/g/metamath/c/5vbEj2vnvAg/m/eJ5qnyS5BQAJ> putting unproved statements of MM100 theorems in set.mm as comments, so that people have an easier time trying to prove these results. Quite often even stating these theorems requires new definitions which are hard to get right. What do you think about having a separate file in the repository with "easier" unproved statements, which do not require new definitions to state or prove? These may serve as a guide on what to do for newcomers (or anyone else), or as a work in progress plan to formalize some big result. 3. If you check the challenge file, you will quickly see that the main part of the proof consists in checking some polynomial identity. Are there any Metamath tools which can prove such statements automatically (by expanding brackets, for example)? -- 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/5e1c4b82-c6df-43b6-bd02-96a808e1a7abn%40googlegroups.com.
