litexlang

5 ms·

1.
by litexlang 9mo 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
2.
by litexlang 9mo 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
3.
Litex: Formal math for everyone – set theory examples with Lean comparison(litexlang.com)
30 points by litexlang 9mo ago|11 comments
4.
by litexlang 9mo 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
5.
by litexlang 1y ago
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
6.
by litexlang 1y ago
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!
7.
by litexlang 1y ago
Working on that bro :)
8.
by litexlang 1y ago
Thank you aktuel!
9.
by litexlang 1y ago
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 m
10.
by litexlang 1y ago
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
11.
by litexlang 1y ago
HAHA, thank you fallat, I guess you are right!
12.
by litexlang 1y ago
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!
13.
by litexlang 1y ago
haha, you are right bro!
14.
by litexlang 1y ago
``` 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, eac
15.
by litexlang 1y ago
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 t
16.
by litexlang 1y ago
Thank you captain! Your observation is pretty interesting! I will fix that after I have more information!
17.
by litexlang 1y ago
Thank you Jon, I will put the semantics and the mathematical system behind online soon! Just give me some time!
18.
by litexlang 1y ago
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 ru
19.
Litex: The First Formal Language Learnable in 1-2 Hours(github.com)
111 points by litexlang 1y ago|82 comments
20.
by litexlang 1y ago
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 re
21.
by litexlang 1y ago
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.
22.
Litex: A simple formal language which 10-year-olds learns quickly(github.com)
1 points by litexlang 1y ago|1 comments
23.
by litexlang 1y ago
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 hand