Incoming links: MongoDB
FeathersJS entry for gothinkster/realworld.
MongoDB-based.
So once you install MongoDB, run with:
MONGODB_FEATHERS_REALWORLD=mongodb://localhost:27017/mydb npm startGot it working on Ubuntu 20.10 with both React and Vue.js front-ends at github.com/randyscotsmithey/feathers-realworld-example-app/commit/8bc3a09242285de624c75bb8345630df499a7d07 as mentioned at github.com/randyscotsmithey/feathers-realworld-example-app/issues/2 except for bad error reporting on UI.
Tests can be run with:but there were 10 failures and 55 passes: github.com/randyscotsmithey/feathers-realworld-example-app/issues/3
MONGODB_FEATHERS_REALWORLD=mongodb://localhost:27017/mydb npm run testCreated by MongoDB, attempts to be even more restrictive than AGPL by more explicitly saying that indirect automatic requests are also included in the "you must give source" domain: opensource.stackexchange.com/questions/8025/difference-between-mongodb-sspl-and-gnu-agpl
The website was dead as of February 2025. Last archive: web.archive.org/web/20240418004442/http://www.themathgenome.com/ Pings:They were seeking help on May 2024:
so its likely the followup death. LinkedIn post gives basic stack: MERN stack, Heroku, Supabase/MongoDB Atlas.
A discussion on the Lean Zulip: leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20Math.20Genome.20Project/near/352639129. Lean people are not convinced about the model in general it seems however.
TODO closed source? Really? www.themathgenome.com/pricing
TODO not viewable without login?
Has conjectures feature.
Built by this dude John Mercer:He must be independently wealthy or something to do such a project? What a hero. But he seems to have jobs. On the side? Hardcore.
A failed Hacker News self post: news.ycombinator.com/item?id=35775071
Ciro Santilli asked: discord.com/channels/1096393420408360989/1096393420408360996/1137047842159079474Owner:So apparently there will be proof checking, but nodependencies between proofs, you still have to pull request everywhing back and face the pain.
Does the website actually automatically check the formal proofs, or is this intended to be implemented at some point? And if yes, is it intended to allow proofs to depend on other proofs of the website (possibly by other people)
Hi Ciro, yes we will be releasing in-browser proof assistant environments/checkers (e.g. Lean). Our goal is not to replace the underlying open-source repos (e.g. Mathlib) so the main dependency will be on the current repos; then when statement formalizations and proofs come in and are certified they can be PR'd to the respective repos. So we will be the source of truth for the informal latex code but only a stepping stone and orchestration layer on the way to the respective formal libraries.
Bibliography: