[smj-edison]

Have you looked at Metamath Zero[1] before? You mentioned using sorts which is what reminded me of it. Just thought I'd point to some additional interesting work :)

[1] https://github.com/digama0/mm0

[geckones]

I didn't thanks for sharing

It looks a cool project, definetely related