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