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!
> Even Kids can formalize the multivariate equation in Litex in 2 minutes, while it [takes] an experienced expert hours of work in Lean 4.
Well, I propose an alternative proof in lean4:
import Mathlib.Tactic
example (x y : ℝ)
(h₁ : 2 * x + 3 * y = 10)
(h₂ : 4 * x + 5 * y = 14)
: x = -4 ∧ y = 6 := by
have hy : y = 6 := by
linear_combination 2 * h₁ - h₂
have hx : x = -4 := by
-- you'd think h₁ - 3 * hy would work, but it won't
linear_combination 1/2 * h₁ - 3/2 * hy
exact ⟨hx, hy⟩
---
One thing I like about the lean proof, as opposed to the litex proof, is that it specifies why the steps are correct. 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?
currently reading through the tutorial. don't have much experience with coq, lean and friends, but this looks like a nice language to get started with formal proofs.
know forall x N: x >= 47 => x >= 17
let x N: x = 47
x >= 17
How does that assumption in the first line have any effect? Surely the underlying theory of naturals should be enough to derive 47 >= 17 ?
And in general I am very skeptical of the claim that Litex "can be learned by anyone in 1–2 hours". Even just the difference between `have`/`let`/`know` would take a while to master. The syntax for functions is not at all intuitive (and understandably so!). & so on. The trivial subset of the language used in the README may be easy to learn but a) it would not get you very far b) most likely every other related toolbox (Lean, HOL, etc) has a similar "trivial" fragment.
But, always good to see effort in this problem space!
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!
Quite flawed, but inspired. This stuff popping up is interesting. I guess it is due to Lean reaching people that would not be aware of formal reasoning on a computer before.
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.
17 comments
[ 2.4 ms ] story [ 35.9 ms ] threadMaking 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!
Well, I propose an alternative proof in lean4:
---One thing I like about the lean proof, as opposed to the litex proof, is that it specifies why the steps are correct. 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?
> Use `have` to declare an object with checking its existence.
an object with what?
https://github.com/enjoy-digital/litex
And in general I am very skeptical of the claim that Litex "can be learned by anyone in 1–2 hours". Even just the difference between `have`/`let`/`know` would take a while to master. The syntax for functions is not at all intuitive (and understandably so!). & so on. The trivial subset of the language used in the README may be easy to learn but a) it would not get you very far b) most likely every other related toolbox (Lean, HOL, etc) has a similar "trivial" fragment.
But, always good to see effort in this problem space!
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!
The simplest formal language is the empty set, which I would argue doesn’t take hours to learn.
So “formal language” is almost certainly not what is meant here, but it’s not clear what else exactly is meant either.