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!
I'm not sure why people don't spend two minutes looking up a quote before sharing it, feels like most people have zero care about quality or polish today, everything is half-assed.
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?
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?)
> Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer.
I learned about the `linear_combination` tactic from your example. Other than that, I use `have` and `exact`, which (a) are not advanced, and (b) are also used in your example.
Before that, my first attempt at the lean proof looked like this:
example (x y : ℝ)
(h₁ : 2 * x + 3 * y = 10)
(h₂ : 4 * x + 5 * y = 14)
: x = -4 ∧ y = 6 := by
-- double h₁ to cancel the x term
have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁]
conv at h₃ => ring_nf -- "ring normal form"
-- subtract h₂ from h₃
have h₄ : (x * 4 + y * 6) - (4 * x + 5 * y) = 20 - 14 := by rw [h₂, h₃]
conv at h₄ => ring_nf
conv at h₁ =>
-- substitute y = 6 into h₁
rw [h₄]
ring_nf
-- solve for x
have h₅ : ((18 + x * 2) - 18) / 2 = (10 - 18) / 2 := by rw [h₁]
conv at h₅ => ring_nf
apply And.intro h₅ h₄
> We are comparing Lean and Litex under conditions where they don’t rely too much on external packages
This proof does have the advantage of not needing to import Mathlib.Tactic. Although again, that's something your proof does.
> how are you supposed to do any nontrivial proofs?
One should also take a look at Isabelle/HOLs AFP here. You can get very far with Metis et al but it is very inefficient computationally.
Especially when proofs get larger and/or layer on abstractions (proving something nontrivial likely involves building on existing algorithms etc.) the ability to make proofs efficient to verify is important.
```
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.
How does it escale for NxN system? Let's say N=10 that is the maximal amount I'd write by hand (in exchange for a lot of money).
I took a look at the example and it's very intuitive. I'm trying to guess which heuristics is it using. Does it try to find exact matches of whatever is inside the parenthesis?
@GP?: Doesn't Lean have a "please fill the blanks" mode for short proof?
> @GP?: Doesn't Lean have a "please fill the blanks" mode for short proof?
Yes, there are several depending on what you want to do. The catchall is `simp` (short for 'simplify').
Why do we need more than one "do what I mean" command? (Or more than zero "do what I say" commands?) Because it's impossible to know what you mean. If you try to use a lot of `simp`, you'll notice that you often have to tell it what to do.
Note that what we really want for this problem is a linear algebra package that can do row reduction, not a formal prover. This problem is all arithmetic.
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!
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.
Yeah, I don't think the authors _actually_ mean that. I think English isn't their first language.
We should try to be charitable (but with a healthy amount of skepticism!); it's possible they meant "Even a child [with a good understanding of Litex] could [mechanically] formalize this multivariate equation in Litex in 2 minutes [as opposed to remembering and writing Lean 4 syntax]"
Kids hardly know what a multivariate equation is. Unless you use "kid" to denote 20-year old college students enrolled in a math program which some people do.
The other claim is doubtful too:
> while it require an experienced expert hours of work in Lean 4.
No, it doesn't. If you have an actual expert, it only takes a few minutes.
And besides, isn't this exactly what an artificial intelligence would solve? Take some complex system and derive something from it. That's exactly what intelligence is about. But LLMs can't deal with the complex but very logical (by definition) and unambiguous system like Lean so we need to dumb it down.
Turns out, LLMs are not actually intelligent! We should stop calling them that. Unfortunately, there are too many folks in our industry following this hyped-up terminology. It's delusional.
Note that I'm not saying LLMs are useless. They are very useful for many applications. But they are not intelligent.
I studied 2x2 linear equation system in high school at 14 (13?) y.o. It was a technical school with more math and physics, and later specialization (like chemistry, electronics, building, ...). I think in a normal school they study that at 16 y.o.
We also teach 2x2 systems to 18 y.o. in the fists year of the university for architects, medics and other degree that don't need a huge amount on math. (Other degrees like engineering or physics get 4x4 or bigger systems that definitively need the Gauss method.)
Unfortunately, whenever you try to exclude LLMs from the holy church of intelligence based on what they can't do, you end up excluding a whole lot of humans too.
Even low-IQ humans can in principle learn how to use Lean to represent a multivariate system. It might take a while, but in principle their brain is capable of that feat. In contrast, no matter how long I sit down with ChatGPT or Gemini or whatnot, it won't be able to. Because they are not intelligent.
It's a great achievement of the AI hype that the burden of proof has been reversed. Here I am, having to defend my claim that they are not intelligent. But the burden of proof should be on those claiming intelligence. The claim that earth is a sphere was extraordinary and needed convincing evidence. The claim that species have evolved through evolution was. But the claim that LLMs are intelligent is so self-evident that rejecting the idea needs evidence? That's upside-down!
> Here I am, having to defend my claim that they are not intelligent.
It's because all you've done is made a claim without any evidence. Someone pointed out a challenge that most claims about them not being intelligent can't submit any evidence that can't also be met by an LLM.
But instead of submitting any evidence to support your claim, you descended into hyperbole about how hard done by you are being expected to support your claims.
In science, it's okay to say we don't know. The amount of disagreement - even amongst smart people - about if LLMs are intelligent or not, suggest to me that we just don't have universally accepted research and definitions that are tight enough to decisively say.
But you're talking not only like you _know_ the answer for sure, so much that you don't need to support it with evidence or credentials, because those who disagree are obviously just poor victims of the AI hype machine.
Please make sure you pass your knowledge of your LLM discoveries onto the scientific community, you could change the world!
Did you read my post? The claim is "LLMs are intelligent". And instead if requiring evidence for that, apparently most folks (including you) are fine with just accepting that claim and require evidence if somebody questions this. That's what I'm doing.
It's like a religion. "God exists" is the claim. Nobody needs to provide evidence that this is not the case. LLMs are intelligent" is the claim. Nobody needs to provide evidence against that. In either case, the burden of proof is with the one making the claim.
> In science, it's okay to say we don't know
But that's not what's happening. LLMs are called "AI". You know what the I stands for, right? It's not "artificial we-don't-know-if-intelligent".
You can write "formal" proofs in this language for mathematical theorems. They are "formal" because they are so detailed that they are machine checkable. That's in contrast to the "informal" pen and paper proofs that people normally produce.
Besides pure maths you can also use that to verify the correctness of software. E.g. say you implemented a shortest path algorithm:
shortestPath(graph, start, end)
You could proof something like:
For all `graph` and each `path` in `graph` from `start` to `end`:
Taking that as the definition, this definitely is not the first formal language learnable in 1-2 hours. I would think, for example, that the language consisting of just the empty string is older and learnable in 1-2 hours.
They probably mean something like “formal language used for writing mathematical proofs that is (about) as powerful as Lean”, though.
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.
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.
It is more likely that the author is not a native english speaker (project author seems to be chinese) and may have used some tool to help with the translation.
I have also been accused of being a Markhov chain, before 2022. I communicate in English only for work and social media so writing may sometimes seem strange to native speakers.
>Litex(website) is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo!). 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 humans and AI is Litex's core mission. This is how Litex scales formal reasoning: by making it accessible to more people, applicable to more complex problems, and usable by large-scale AI systems. These benefits stem from Litex's potential to lower the entrance barrier by 10x and reduce the cost of constructing formalized proofs by 10x, making formal reasoning as natural as writing.
>Even Kids can formalize the multivariate equation in Litex in 2 minutes, while it require an experienced expert hours of work in Lean 4. It is a typical example of how Litex lowers the entrance barrier by 10x, lowers the cost of constructing formalized proofs by 10x, making formalization as easy and fast as natural writing. No foreign keywords, no twisted syntax, or complex semantics. Just plain reasoning.
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!