[Litex](https://litexlang.com) is a simple open-source computer language for mathematical proofs. Anyone can have a rough understanding of Litex in 2 hours.
Although it is not yet ready for production use, it is already powerful enough to formalize set theory and basic logic, which is enough for most daily mathematical proofs. Visit [Set Theory Examples](https://litexlang.com/doc/How_Litex_Works/Litex_vs_Lean_Set_...) for more examples.
Something that always bugged me about Lean is how unreadable and unwritable.
Math uses extremely heavy notation to make statements concise. It's hard to learn the notation without a visual reference guide, sync the symbols don't have guessable names, but once you know what the symbols mean, it's readable.
Java is incredibly verbose but you can make out what it's saying word by word
Lean is line noise. It's like assembly language for math, which is great, but not what humans should be using day to day.
This Litex does a nice job of being concerned about humans reading and writing the code.
Do you have an example Lean statement you struggle with? I would have posed that they're "just" using standard math notation that should be explained in the relevant textbook for the math you're trying to formalize, but perhaps they are indeed cooking...
One thing I never understood about this: why does this not just compile to Lean so they're compatible with each other? Having a good interface is admirable, but the difference between set and type based foundations seems not very important and porting any enough math to sustain Litex seems like a huge undertaking.
8 comments
[ 3.2 ms ] story [ 25.5 ms ] threadAlthough it is not yet ready for production use, it is already powerful enough to formalize set theory and basic logic, which is enough for most daily mathematical proofs. Visit [Set Theory Examples](https://litexlang.com/doc/How_Litex_Works/Litex_vs_Lean_Set_...) for more examples.
Star the repo [here](https://github.com/litexlang/golitex) to support Litex, and join our [Zulip community](https://litex.zulipchat.com/join/c4e7foogy6paz2sghjnbujov/) to give us feedback and suggestions!
Happy Christmas
Math uses extremely heavy notation to make statements concise. It's hard to learn the notation without a visual reference guide, sync the symbols don't have guessable names, but once you know what the symbols mean, it's readable.
Java is incredibly verbose but you can make out what it's saying word by word
Lean is line noise. It's like assembly language for math, which is great, but not what humans should be using day to day.
This Litex does a nice job of being concerned about humans reading and writing the code.
[如何评价 Litex 语言？ - 知乎](https://www.zhihu.com/question/1965786839827854197)