John Mercer (Jul 17 2023 at 01:07): John Mercer (Jul 17 2023 at 01:07):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 Coq, Lean, HOL, or 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 and our Twitter announcement 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 Coq community.
Best,
John
Karl Palmskog (Jul 17 2023 at 10:33):one relevant set of questions is hinted at in the LinkedIn post comments: how are copyright issues handled, e.g., w.r.t. existing (Coq) code that is presumably available in the web platform and any changes done by users to this code?
For the record, the project and its data is from what I can see inaccessible without an account, which (in my experience) is likely to be viewed skeptically by community members working mostly on publicly accessible web platforms.
John Mercer (Jul 17 2023 at 23:38):Hi @Karl Palmskog , thanks for the question! I should have learned by now to address this question early and clearly.
Symbiosis and Separation of Concerns of TMGP and Formal Repos
Based on discussions with the Lean community, we changed course and chose to separate the concerns between mathlib -- and all other OS repos -- and focus on being the marketplace and informal-formal integration on top of all the repos.
You'll notice that currently the bounty system is functional only for informal proofs. The formal content (to seed the platform) is sort of a 1st order approximation to help users see -- for the first -- a large scale integrated database of informal and formal proofs side-by-side. As we continue generalizing the bounty system and enable statement and proof formalizations in a variety of languages, we will focus on marketplace activity and only perhaps show statement and proof previews and then link to the respective formal repo. When new proofs created through platform activity have a bigger blast radius in the repos (restructuring/redesign), it gets trickier for submission and credit but we'll work through these things based on formal community feedback.
We're targeting deploying in 2 weeks the generalized bounty system for statement/proof formalization.
Public vs Login
TMGP is a marketplace and a social platform where identity matters – it’s a place for recognizing your passion, hard work and ideas (i.e. attribution). Similar to Zulip, this isn't possible unless people verify who they are.
An important reminder though: even though you have to login, all content (informal/formal) is free and always will be.
Ana de Almeida Borges (Jul 18 2023 at 00:05):This Zulip currently requires a log-in to comment on, but not a log-in to view. I think that's a good model that balances the content being (trivially) publicly accessible and attribution. Can you do something like that?
John Mercer (Jul 18 2023 at 03:18):Also wanted to invite tenured professors in FR to consider joining as a Founding University Partner. I'm capping this group and only adding 1-3 more, and would like to get one INRIA representative. You can schedule directly from the website to meet with me.
John Mercer (Jul 27 2023 at 06:56):Hi @Ana de Almeida Borges , thanks for the feedback! We're planning on opening up the Search/View to public and then only if you want to participate to login. We are finishing a sprint right now and it's planned for the next sprint (so ~ 2 weeks).
John Mercer (Jul 31 2023 at 10:18):Hi all,
A new MGP release is out.
@Karl Palmskog , hope this helps resolve your previous question.
@Ana de Almeida Borges @Michael Soegtrop @Paolo Giarrusso , the next release will add public content and also a User Profile Page: Separate from your account page, this optionally public page acts as a portfolio to highlight your contributions. We hope this profile page becomes a staple in resumes to highlight contributions.
The new tour will walk you through all the features at login, but I’ll highlight a few things here.
Our goal with this release is to go from neat concept illustration to a more intuitive, functional and generalized platform for both peer-to-peer and institutional grant funding that accelerates mathematical discovery by leveraging the power of a broader community.
Updates
Projects: You can now visualize the project status checklist for each statement, and the current open projects for each statement (open to both submissions and funding). Let us know what you think! We wanted to demystify and answer the question “So what can I do?!”
Search: More advanced search options for different statements, and a summary progress bar in the search results table to help you quickly assess where you can make an impact.
Creation: Revamp of the Statement creation page that lets you add expository notes, references and even a YouTube link for an explainer video. We have one, and possibly two, new entries coming online that include an explainer video on the history of the open problem being funded.
Teams: You can now form teams, and submit projects on behalf of a team. The team can decide how grant award %'s should be allocated to each teammate, and the team leader can make the allocations.
Dashboard: The new dashboard lets you quickly see platform stats and find the most popular statements, grant activity and most recent activity.
About Page: Not exciting from a feature perspective, but it was in desperate need of an update to help people understand the mission we're on.
Along with this, we have what is shaping up to be over $10,000 in new grants coming on line in the coming weeks and our goal is to get to $1,000,000 in grants this year to fund curation (for known math), new proofs/solutions, and formalization projects in Lean, Coq, HOL, and Metamath.
One other thing you'll notice is that we've departed from using the term "bounty."
Any questions or comments please let me know.
John Mercer (Aug 15 2023 at 21:49):Another update folks! @Karl Palmskog et al, you can now browse TMGP without logging in. https://www.themathgenome.com/
Michael Soegtrop (Aug 16 2023 at 11:01):One still can't view submitted proofs without login, though.
Last updated: Oct 13 2024 at 01:02 UTC