Litex: The First Formal Language Learnable in 1-2 Hours

[litexlang]

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!

[anonzzzies]

Lisp is pretty practical even though not many people use it anymore.

[ccppurcell]

"Never believe quote attributions given on the internet" - Abraham Lincoln

[CaptainOfCoit]

The quote from the README seems indeed to be falsely attributed to da Vinci. The quote in question:

> Simplicity is the ultimate sophistication. - Leonardo da Vinci

https://checkyourfact.com/2019/07/19/fact-check-leonardo-da-...

https://quoteinvestigator.com/2015/04/02/simple/

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.

[cbdevidal]

“Arrrg! I’ve seen that quote everywhere! I must put a stop to this.” - John Wilkes Booth

[litexlang]

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!

[thaumasiotes]

> 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?

[JonChesterfield]

The website tells me it's simple over and over but not what it is. What're the semantics? Which mathematical system is this? What can it prove?

[tverbeure]

LiteX has been a digital SOC IP library for man years.

https://github.com/enjoy-digital/litex

[lou1306]

I got kind of lost at this part of the tutorial (https://litexlang.com/doc/Tutorial/Know):

    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!

[litexlang]

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

[litexlang]

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

[kuruczgy]

So Litex is not based on Type Theory I gather. How are proofs represented and checked?

[two_handfuls]

This looks potentially interesting. The "cheat sheet" seems the most useful document listed but it lost me there:

> Use `have` to declare an object with checking its existence.

an object with what?

[card_zero]

With checking-its-existence. With checking of its existence. With existence checking. While checking its existence. OK it could be better written.

[aktuel]

The tutorial explains the language in much more detail: https://litexlang.com/doc/Tutorial/Introduction

[litexlang]

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!

[blubber]

How did you formally test this claim: "Even Kids can formalize the multivariate equation in Litex in 2 minutes"

[fallat]

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

[Dilettante_]

Reminded me of that article about hoobastanking the Snarfus from a couple days back[1]. And xkcd 2501, of course.

[1]https://anniemueller.com/posts/how-i-a-non-developer-read-th...

[teiferer]

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.

[jokoon]

What's a formal language?

[ngruhn]

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`:

    path.length <= shortestPath(graph, start, end).length

[Someone]

The only definition I know of is https://en.wikipedia.org/wiki/Formal_language. I also think that is the commonly accepted definition.

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.

[auggierose]

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.

[litexlang]

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.

[layer8]

The title seems to be misusing the term “formal language”: https://en.wikipedia.org/wiki/Formal_language

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.

[lorenzohess]

Can Litex and Lean be transpiled?

[litexlang]

Working on that bro :)

[aktuel]

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.

[ngruhn]

fyi: they finally renamed Coq. It's called Rocq now.

[litexlang]

Thank you aktuel!

[Almondsetat]

This github README is written by an LLM.

[aktuel]

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.

[litexlang]

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!

[jasonjmcghee]

I doubt it? And if it is, honestly best LLM readme I've seen. What makes you think so?