Litex is a set-theory based, fact-oriented formal language trying to lower the barrier to entry of reading and writing formal math code. A great feature of Litex is that the user can write what to prove and it's the language itself that searches and tells you how it is prove, which means Litex automatically maps out the structure of math for you. It also has an expanding compiler translating Litex to Lean. The source code is open-sourced https://github.com/litexlang/golitex

Moreover, Litex aims for more than simpler syntax, it wants to align formal code semantics to daily math: for example, in lean, 1 / 0 returns 0, (1 : Nat) - 2 returns 0. These are very strange to normal people. Litex tries to eliminate the gap between formal code and "real math".