litexlang

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.

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

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

have is used to ensure the existence of the object you define. For example, you do not want to declare a new object when it is from an empty set!

haha, you are right bro!

``` If litex's strategy is "you describe the steps you want to take, and litex will automatically figure out why they're correct", how are you supposed to do any nontrivial proofs? ```

HAHA, what i am saying here is, each statement you write, is automatically checked by Litex, using its known specific facts and universal facts. Since any math proof, no matter complex or simple, can be divided into many small steps and each small step can be verified in that way, I guess it is fair to say "automatically figure out why they're correct" to a non-mathematicl person when introducing Litex.

Thank you thau! Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. We are comparing Lean and Litex under conditions where they don’t rely too much on external packages, which makes the comparison a bit fairer. (since Lean does have a very rich set of libraries, but building libraries is itself a challenge. Litex really needs to learn from Lean on how to build a successful library!).)(afterall, Litex can also abstract all proofs here and give it a name linear_combination, right?)

Thank you captain! Your observation is pretty interesting! I will fix that after I have more information!

Thank you Jon, I will put the semantics and the mathematical system behind online soon! Just give me some time!

Hi there! I am jiachen shen, creator of Litex.

I feel really lucky that Litex has drawn so much attention from you guys! I always like the geek culture of HN, and have absolutely no idea why such a random guy from a random background can rush into the top 10 on Hacker News.

Litex gets its name from Lisp and LaTeX. I want to make Litex as elegant and deep as Lisp, and at the same time as pragmatic as LaTeX.

Many people have raised questions and suggestions about Litex, and I’m truly grateful. Since I’m developing the Litex core on my own, a lot of the documentation is still incomplete — I’ll try my best to improve it soon! All of your suggestions are really helpful. Thank you so much!

Litex is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo! https://github.com/litexlang/golitex). It ensures every step of your reasoning is correct, and is actually the first reasoning formal language (or formal language for short) that can be learned by anyone in 1–2 hours, even without math or programming background.

Making Litex intuitive to both human and AI is the mission of Litex. That is how Litex scales formal reasoning: making it accessible to more people, applicable to more complex problems, and usable by large-scale AI systems.

The comparision between Litex and Lean is on our website(https://litexlang.com). There is also a straightforward tutorial about it on our web that you do not want to miss.

Contact me if you are interested! Really hope we can scale formal reasoning in AI era together!

Sorry for your story. In those days open source is REALLY HARD. Put your github link here and we will support your project by starring you and spreading your project. You definitely need to fight back.

Hi everyone!

I'm excited to introduce Litex — a simple formal language designed to make mathematical formalization accessible to everyone, even 10-year-old beginners! With 2,800 GitHub commits and growing, Litex is now capable of handling real mathematical examples. My name is Jiachen Shen, and as a passionate language design geek, I've created Litex to bridge the gap between abstract formal systems and human intuition. Get Involved Today!

GitHub (Star us! ):

https://github.com/litexlang/golitex

Try Litex Online:

https://litexlang.org/playground

Join Our Community:

https://discord.gg/uvrHM7eS

Contact: [litexlang@outlook.com](https://mailto:litexlang@outlook.com/)

Your feedback, ideas, and contributions are not just welcome - they're essential to our journey. Let's make formal mathematics accessible together!