5 ms·

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

• litexlang 1y ago
  Litex is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo! https://github.com/litexlang/golitex 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 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!
  • JonChesterfield 1y ago
    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?
    • litexlang 1y ago
      Thank you Jon, I will put the semantics and the mathematical system behind online soon! Just give me some time!
  • thaumasiotes 1y ago
    > 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?
    • c0balt 1y ago
      > 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.
    • 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 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?)
      • thaumasiotes 1y ago
        > 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.
• Almondsetat 1y ago
  This github README is written by an LLM.
  • jasonjmcghee 1y ago
    I doubt it? And if it is, honestly best LLM readme I've seen. What makes you think so?
    • Almondsetat 1y ago
      >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. Boilerplate and constant repetition
      • tux3 1y ago
        Humans are perfectly capable of doing that on their own. The random parentheticals and the sentence structures are very human to me.
      • jibal 1y ago
        No LLM would write that without prompting it to be illiterate in English.
  • aktuel 1y ago
• kuruczgy 1y ago
  So Litex is not based on Type Theory I gather. How are proofs represented and checked?
• lorenzohess 1y ago
  Can Litex and Lean be transpiled?
  • litexlang 1y ago
    Working on that bro :)
• blubber 1y ago
  How did you formally test this claim: "Even Kids can formalize the multivariate equation in Litex in 2 minutes"
  • fallat 1y ago
    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]"
    • litexlang 1y ago
      HAHA, thank you fallat, I guess you are right!
  • teiferer 1y ago
    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.
    • exe34 1y ago
      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.
• ccppurcell 1y ago
  "Never believe quote attributions given on the internet" - Abraham Lincoln
  • cbdevidal 1y ago
    “Arrrg! I’ve seen that quote everywhere! I must put a stop to this.” - John Wilkes Booth
    • Smoosh 1y ago
      “I believe John Wilkes Booth to be innocent!” - Alexander Hamilton.
  • CaptainOfCoit 1y ago
    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-vinci-simplicity-ultimate-sophistication/ https://checkyourfact.com/2019/07/19/fact-check-leonardo-da-... https://quoteinvestigator.com/2015/04/02/simple/ 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.
    • litexlang 1y ago
      Thank you captain! Your observation is pretty interesting! I will fix that after I have more information!
• two_handfuls 1y ago
  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 1y ago
    With checking-its-existence. With checking of its existence. With existence checking. While checking its existence. OK it could be better written.
    • litexlang 1y ago
      haha, you are right bro!
  • aktuel 1y ago
    The tutorial explains the language in much more detail: https://litexlang.com/doc/Tutorial/Introduction https://litexlang.com/doc/Tutorial/Introduction
  • 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!
• jokoon 1y ago
  What's a formal language?
  • ngruhn 1y ago
    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 1y ago
    The only definition I know of is https://en.wikipedia.org/wiki/Formal_language 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.
• tverbeure 1y ago
  LiteX has been a digital SOC IP library for man years. https://github.com/enjoy-digital/litex https://github.com/enjoy-digital/litex
  • almostgotcaught 1y ago
    [flagged]
    • tverbeure 1y ago
      That’s a lot of words and anger for such a small thing.
      • deleted 1y ago
        [deleted]
      • almostgotcaught 1y ago
        It's a low brow dismissal of someone's work? How else should I react?
        • majorchord 1y ago
          this might shed some light on what's wrong: https://0x0.st/KB-b.txt https://0x0.st/KB-b.txt
          • almostgotcaught 1y ago
            > Hacker News users don’t see you... Lolol I sure hope no one hn sees me as anything (otherwise it's past due for me to dump this handle).
          • FrustratedMonky 1y ago
            where can i generate that analysis?
            • 1y ago
• aktuel 1y ago
  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 1y ago
    fyi: they finally renamed Coq. It's called Rocq now.
    • CaptainOfCoit 1y ago
      Guess they had to change the logo too? Just because evangelical anglophone users couldn't get past the name sounding like "cock" or what?
      • ngruhn 1y ago
        Yes, but I don't think it has anything to do with evangelicalism. It's just like Uranus. You can't talk about without it always being a bit unserious.
  • litexlang 1y ago
    Thank you aktuel!
• lou1306 1y ago
  I got kind of lost at this part of the tutorial (https://litexlang.com/doc/Tutorial/Know 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 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
    • lou1306 1y ago
      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.
  • 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 make x >= 17 here, so ``` know forall x N: x >= 47 => x >= 17 ``` is essential
• 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 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 1y ago
    Lisp is pretty practical even though not many people use it anymore.
• auggierose 1y ago
  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 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 to programming.
• layer8 1y ago
  The title seems to be misusing the term “formal language”: https://en.wikipedia.org/wiki/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.