litexlang

Joined 1 year ago

Karma

Submissions

Member since

May 24

Recent submissions

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

Comment · 18 days ago

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

Litex: A Formal Language as Easy to Learn as Python and LaTeX litexlang.com

1 litexlang 18 days ago 2 comments

Comment · 10 months ago

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.

Comment · 10 months ago

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

Comment · 10 months ago

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