It's truely great if Litex does compile to existing formal languages. The only problem is that we can not find a good way to compile our verification process, which does not require users to give names to facts they are using and thus very different from how Lean works, to Lean (set theory example is just the first one of a series of comparisons). Besides, it's even harder to compile future functionaliteies, like printing out results of each statement of litex in a human readable way, to lean. So since litex is still a young language and we are using our limited resources to try new ideas and crack here and there, for the time being we believe it's not a good time to migrate our code in such a great scale. Thank you. Merry Christmas.

To be honest I'm not convinced by the technical downsides you mentioned here BUT I can see why you wouldn't want to spend time on this if it takes away from language development. Thanks!

Thanks! It seems the font color defers in different systems (I did not find this behavior on my machine). So I changed the font color to pink :)

Happy Christmas

[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.

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!

Thank you auggierose. Your comment is by far the best description of the stage of Litex is now: very flawed, but very different from other formal languages. I guess it is because Litex is closer to reasoning (or math in general) rather than to programming.

haha, no, it is not. visit my git commits and you can see the readme has been updated ~1000 times! I really want my readme look good!

Working on that bro :)

Thank you aktuel!

know @self_defined_axiom_larger_equal_is_transitive(x, y, z R): x >= y y >= z =>: x >= z

Since transitivity of >= is not implemented, one has to call this self_defined_axiom_larger_equal_is_transitive to make x >= 17 here, so

``` know forall x N: x >= 47 => x >= 17 ```

is essential

The first line is essential, because Litex does not implement transitivity of >= in its kernel and one has to formalize it: know @larger_equal_is_transitive(x, y, z R): x >= y y >= z

Thank you for clarifying, but don't you think this puts a rather big dent in the claim that Litex is "intuitive" and "can be learned by anyone in 1–2 hours"? I think the average user would expect the natural/real numbers to come equipped with this kind of theorems.

For instance, the tutorial says that "The daily properties" (whatever this means) of "+, -, , /, ^, %" are "already in the Litex kernel". What about associativity of and +, or distribution of * over +? Are these part of the "daily properties"? And if so, why didn't transitivity of >= not make the cut?

Just trying to understand the design choices here, this is very interesting.

HAHA, thank you fallat, I guess you are right!