On Sat, Nov 21, 2020 at 11:52 PM Jim Kingdon <[email protected]> wrote:
> Mario Carneiro wrote: > > > If there is enough interest from others that I'm not the only one on the > project, I don't mind taking the lead here. > > I suppose this is the time to express interest or lack of interest. I > will express a small amount of interest. In terms of the value of the > concept, the interest comes from the idea that I can think of various > things (new features, cleaning up various rough edges, fixing buggy or > odd behaviors, etc) we might want which aren't in metamath.exe or mmj2 . > And that those two codebases - for all their usefulness - are I suspect > hitting a bit of a limit in terms of whether you'd want to want to do a > lot of new development to them. > I don't think it's important that the project get to critical mass in the near term. Building a theorem prover is a long term project. The main goal here is to have a place where people can feel comfortable collaborating. I will chip in when I can with the time that I have, and it doesn't take a whole lot of additional participation for it to become the "place to go" if you are interested in improving the metamath experience generally. Once we have that, it will grow at a natural pace as these things do. The hard part, as you point out, is getting past the point where it is viewed as one person's project. Even just issues are useful if you don't want to get in on the software side. Lean 3 community development is an interesting parallel. After Leo left to work on lean 4, progress on the lean 3 codebase went into a freeze for about a year, until eventually we had picked up too many bugfix workarounds in mathlib, and eventually we opened up the "community edition", which has seen development by 6 or so people. Certainly much less than the 80-some working on mathlib, but enough to keep it alive and release another 19(!) versions. To me that is what a healthy state of development looks like. Metamath has much fewer contributors, but there are enough users to keep the issues coming, and one or two part-time developers is more than enough to make progress. Mario -- 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/CAFXXJSvB-47Qn%3DQEtfebUgWaqRaL8kjo6jitM%2BtoW2R4m394qQ%40mail.gmail.com.
