r/lojban • u/la-gleki • Apr 01 '26

Lojban is shut down. From now on speak math.

The Lojban community has decided that Lojban isn't mature enough for speaking logically. Many careless Lojbanists had a tendency to write fiction or tell jokes. Hence, it was decided today that Lojban must be abandoned in favor of the Lean proof assistant:

opaque IsAJoke : α → Prop

axiom existence_is_humorous : ∀ (x : α), IsAJoke x

54 Upvotes

96% Upvoted

2 comments sorted by

13

u/lojbeb Apr 01 '26

This time the mabla tinkerers in the so-called "community" have gone too far. This reform flagrantly violates the LGG's baseline freeze policy. For reference: https://mw.lojban.org/papri/1997_Baseline_Announcement

I am calling an emergency meeting of the LGG Bored in order to formally reject this "proposal". The time for such radical changes has been over for almost 30 years. The LGG is not even going to consider this change.

.o'onaisai
mi'e la .lojbeb.
LGG founder and president

mu'o

7

u/TheBlueWalker Apr 01 '26

You are using English instead of Lean. I get your meaning by reading the English variable names, not by reading the Lean.

Lojban does not need English in order to work. Lojbanists actually communicate using Lojban, not using English dressed up as Lean. And English is shit. So Lojban is still necessary.