Re: [Metamath] brismu: a relational interpretation of Lojban

['David A. Wheeler' via Metamath]

> On Jan 2, 2025, at 9:48 PM, mostawe...@gmail.com <mostawesomed...@gmail.com> 
> wrote:
> Hi friends,
> I have gone long enough without letting this group know about a project of 
> mine: la brismu, a living book which presents the constructed language Lojban 
> as a logic. About two thirds of la brismu is written in Metamath, providing a 
> computer-verified basis for trusting various high-level statements.
> ...
> A living version of la brismu is published online [0]. Collaboration is 
> invited on GitHub [1]. Thanks for reading! ...
> [0] https://brismu.systems/
> [1] https://github.com/brismu/brismu

Wow. That's amazing.

I think there should be a link from some of our Metamath pages to this work, so 
that
those interested can learn about it. I'm not sure where or what it should say.
Yet I think the fact this even *exists* is quite remarkable.

Thank you for sharing about this!

--- David A. Wheeler

-- 
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 metamath+unsubscr...@googlegroups.com.
To view this discussion visit 
https://groups.google.com/d/msgid/metamath/84941615-09BE-40F5-89A5-035724B8883F%40dwheeler.com.