At one stage I had high hopes for Raph Levien’s “ghilbert”, which was a reworking of Metamath to iron out a couple of problems and make it easier to work on problems in a distributed, cooperative way, but now even its domain doesn’t seem to work.
Metamath does seem to me closest to the ideal. I’m still trying to make sense of this stuff now.
At one stage I had high hopes for Raph Levien’s “ghilbert”, which was a reworking of Metamath to iron out a couple of problems and make it easier to work on problems in a distributed, cooperative way, but now even its domain doesn’t seem to work.
Metamath does seem to me closest to the ideal. I’m still trying to make sense of this stuff now.