Hi Steven, Thanks for the feedback! You're right. In the walkthrough we should really add a note that right now we only allow for informal proofs. Our next deployment in 2 weeks will allow for three types of projects: curation (statement and proof exists, but tracking it down and/or LaTeX code procurement), new informal proof, and formalizations.
Regarding the $$$$. Thanks for the LOL regarding "hodgepodge" :-) Will include a fix in this sprint! Best, John On Sun, Jul 16, 2023 at 2:34 PM Steven Nguyen <[email protected]> wrote: > I don't see a way to submit a formal proof. > > While submitting a non-candidate proof I tried to create a newline in > various ways, such as " > > " (two actual newlines), "\\", "\newline", "\(\newline\)", and > "\displaylines{ a \\ b }" but nothing worked. > So I had to use a hodgepodge empty math block ("$$$$") which is less than > ideal. > [image: Screenshot 2023-07-16 132708.png] > On Saturday, July 15, 2023 at 1:32:16 AM UTC-5 [email protected] wrote: > >> Wonderful thank you for the feedback! >> Best, >> John >> >> >> On Thu, Jul 13, 2023 at 1:48 PM Discher, Samiro < >> [email protected]> wrote: >> >>> Hi John, >>> >>> I very much like the concept and will curiously follow if it will work >>> out. Even though, being a theory and tools builder myself, solving popular >>> problems (or other people's problems outside my core interests) is just not >>> what I (currently) want to do. >>> >>> Some issue I immediately noticed when trying to fill out my profile is >>> that the "Research tags" text field is not as wide as it should be (the >>> border is much wider): >>> >>> Also, when I uploaded a profile picture, all text fields *except* >>> "Research tags" got cleared out so that I had to fill them again. After >>> saving, information inserted into "Research tags" got lost. I used Firefox >>> 115.0.1 >>> (64-Bit) on Windows. >>> The website definitely needs polishing. >>> >>> — Samiro Discher >>> ------------------------------ >>> *Von:* [email protected] <[email protected]> im Auftrag >>> von Johnathan Mercer <[email protected]> >>> *Gesendet:* Donnerstag, 13. Juli 2023 02:18:34 >>> *An:* Metamath >>> *Betreff:* [Metamath] The Math Genome Project - feedback request >>> >>> Hi all, >>> >>> I'd really appreciate your feedback on The Math Genome Project. >>> >>> Our goal is to provide the 1st marketplace and social platform for >>> higher mathematics. Where anyone can make a living (or a serious >>> side-hustle) doing proof curation, writing, and formalization projects in >>> any of the leading languages like Metamath. >>> >>> A big motivation was empowering respective formal communities and create >>> opportunities for paid formalization projects -- so people can spend more >>> time doing what they love. >>> >>> The website is here: https://www.themathgenome.com/ >>> Here is the LinkedIn post >>> <https://www.linkedin.com/posts/johnmercer_mathematics-generativeai-activity-7084671465488281600-3rxe?utm_source=share&utm_medium=member_desktop> >>> and >>> our Twitter announcement >>> <https://twitter.com/TheMathGenome/status/1678909712027320320> if you'd >>> be so kind to re-post/tweet to help spread the word. >>> >>> Look forward to your feedback and feature requests in general (informal >>> or formal side) and specific things we can do to help the Metamath >>> community. >>> >>> Best, >>> John >>> >>> >>> -- >>> 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/b2d15400-66d5-42a1-b33c-4b77ed0154e7n%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/b2d15400-66d5-42a1-b33c-4b77ed0154e7n%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >>> -- >>> 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/57cb7257aaf84862a2bbd2fec327f44f%40rwth-aachen.de >>> <https://groups.google.com/d/msgid/metamath/57cb7257aaf84862a2bbd2fec327f44f%40rwth-aachen.de?utm_medium=email&utm_source=footer> >>> . >>> >> -- > 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/f003301d-ccaf-499f-94b0-02cbcca2bc75n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/f003301d-ccaf-499f-94b0-02cbcca2bc75n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAHvyvqqCgut7X_%3DgBatqgH%3DS5YNe1oATZOiUEVm3%3D4btzpnxhw%40mail.gmail.com.
