Litex: The ‘Too Easy’ Formal Language Even Kids Can Master

Stream: general

[Jackie Shen]

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! :rocket: With 2,800 GitHub commits and growing, Litex is now capable of handling real mathematical examples. My name is Jiachen Shen, and as a passionate language design geek, I've created Litex to bridge the gap between abstract formal systems and human intuition.

Why Litex Stands Out

:sparkles: Designed for Humans First

• Built from the ground up to mirror how we naturally think about math
• Eliminates complex programming concepts like variables and control flow

:search: Math-Specialized Design

• Unlike Lean (a Turing-complete system), Litex is a read-only Turing machine
• Uses intuitive pattern matching and substitution - just like human reasoning
• Think of it like SQL for databases, but for everyday math! This is a domain language specialized and focuses on math.

:seedling: Growing Community Project

• Started as a solo endeavor, now opening to community contributions
• Help shape the future of: kernel development, real-world adoption, and new features
• Still under development, not ready for production use. Your help is invaluable for Litex!

Get Involved Today!

:computer: GitHub (Star us! :star:):

https://github.com/litexlang/golitex

:desktop_computer: Try Litex Online:

https://litexlang.org/playground

:umm: Join Our Community:

https://discord.gg/uvrHM7eS

:e-mail: Contact: litexlang@outlook.com

Litex isn't here to replace Lean, but to offer a simpler alternative where full Turing-completeness isn't needed. If you've ever been curious about formal reasoning but intimidated by complex systems, Litex is your gateway! Your feedback, ideas, and contributions are not just welcome - they're essential to our journey. Let's make formal mathematics accessible together! :glowing_star:

Comparison With Lean4
Example: Syllogism
Example: Definition of Algorithm
Example: Multivariate System of Linear Equations

[Aaron Liu]

I think I broke it...

0 / 0 = 0
0 / 0 = 1
0 = 1

[Jackie Shen]

Aaron Liu said:

I think I broke it...

0 / 0 = 0
0 / 0 = 1
0 = 1

OH! Than you Liu. The natural number system are builtin in Litex and their logic is separate from the "match and substitute" system of Litex. I think I broke this number system a few days ago and forget to fix them. I WILL FIX THEM IMMEDIATELY THIS DAY. REALLY APPRECIATE YOUR FEEDBACK!

[Jackie Shen]

Aaron Liu said:

I think I broke it...

0 / 0 = 0
0 / 0 = 1
0 = 1

This Bug fixed bro. Thank you for your kind comment!

[Shreyas Srinivas]

How exactly is this different from the prolog family of languages?

[Kyle Miller]

Maybe you should say what you see as being similar to Prolog-like languages @Shreyas Srinivas?

[Shreyas Srinivas]

A few things:

1. it speaks of itself as an SQL of some sort.
2. The entire tutorial. It reads like a logic programming language with support for checking and inference in first order logic.

EDIT: logic oriented programming languages are the subject of a fairly lively area of research. See “Answer set programming” for example.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

I am trying to understand where this fits into that picture, because such languages are already capable of succinctly expressing propositions and performing sophisticated checking and even synthesis.

[Jackie Shen]

Shreyas Srinivas said:

How exactly is this different from the prolog family of languages?

Thank you for your attention Srinivas! Prolog is a programming language, and it is a turing machine. Litex is NOT a programming language, it is a read-only turing machine. There is no control flow, variable, execution in Litex. ANYTHING Litex does for you is 'match and substituion'. Think of Litex as a very fancy “Find or Search (ctrl+f on windows, cmd+f on mac)", that is how litex verifies a statement!

[Notification Bot]

This topic was moved here from #general > Litex: A Human-Friendly Formal Language by sanyan.

[Jackie Shen]

Shreyas Srinivas said:

A few things:

1. it speaks of itself as an SQL of some sort.
2. The entire tutorial. It reads like a logic programming language with support for checking and inference in first order logic.

EDIT: logic oriented programming languages are the subject of a fairly lively area of research. See “Answer set programming” for example.

Hello. Last week you asked about the difference of Litex(https://github.com/litexlang/golitex) and Prolog. Here are similarities and difference between those 2 languages:

Similarities:

1. Both of them uses match and substitute to derive new facts from existing facts. They both can express existence and universal quantification.

Differences:

1. Unknown facts are by default false in Prolog, while in Litex, they are by default unknown. This is a very important difference. Since what can not say a claim must be false even if nobody can prove it for the time being, we can not say a claim that is not known to be true must be false.

2. Litex is not a programming language. Prolog is a programming language.

3. Prolog does not have a type system, making it hard to express set theory, which is the foundation of mathematics. This makes translation from natural language to Prolog unimaginably hard. Litex by design has a set system that is very easy to use.

4. Compared to Litex, Prolog is still too complicated and foreign to most people, partly because it is a programming language. The biggest strength of Litex is that its extremely deep insight into the nature of math and its extremely simple design to make the language as natural as possible. Just like you can use Python or Assembly to write a program and in most cases, Python is easier to use, Litex is easier to use than Prolog.

5. Technical difference: 1. exist proposition must be given a name in Litex and it is user's duty to specify which object satisfy the proposition requirement. 2. prolog might encounter dead lock when proving iff condition, and Litex avoids infinite search by setting the upper bound of searching to 2 layers. 3. In Litex, you can express forall facts without giving it a name, while Prolog forces you to do so.

Thank you for your feedback. Join our zulip https://litex.zulipchat.com/ and star our repo for more information about future development of Litex!

[(deleted)]

I can smell a LLM from a distance... Sorry but I'm kinda tired of people using LLMs to churn out boring looking posts

[(deleted)]

If you can type a prompt into a LLM you can write a message directly here and it takes the same amount of effort

[(deleted)]

As for the language I think it's an interesting concept. But I can see a few unfair comparisons in the readme file

[(deleted)]

And I don't understand what you mean by Turing complete in this context

[Niels Voss]

Huỳnh Trần Khanh said:

I can smell a LLM from a distance... Sorry but I'm kinda tired of people using LLMs to churn out boring looking posts

I think this is a bit unfair. The points about facts being false vs unknown by default actually seems quite important, and the comparison is overall very useful. That being said, I do agree some of the comparisons in the readme feel a bit unfair (for example, Lean does have proof search via tactics, and it does have some built-in math without requiring external libraries)

[suhr]

Learning Curve
Lean4: High (The prerequisites are very high even for PhD students)

In my opinion, the difficulty of leaning Lean is grossly overstated. Also it requires basically no prerequisites, only the right point of view.

[Arthur Paulino]

I agree that learning Lean is not an easy task, but I don't think it has anything to do with a formal degree. The "problem" is that Lean 4 is an extremely broad and wide system, in which you can do regular programming tasks, theorem proving, programming mixed with theorem proving, FFI, meta programming etc. And each use case is a world in itself.

[suhr]

Well, that's actually a half of a problem (the programmer's half). Another half is that while the core of Lean is a few simple rules, proving things is rarely a straightforward application of them. You quickly find proving even a simple statement hopeless unless you define a bunch of lemmas, and these lemmas also might need some lemmas to prove, and so on... And then you need to skillfully combine all the lemmas you need.

And while automation can help quite a bit with that second half, it can't solve it completely.

[Jackie Shen]

Huỳnh Trần Khanh said:

I can smell a LLM from a distance... Sorry but I'm kinda tired of people using LLMs to churn out boring looking posts

Hi Khanh， thank you for your comment. I am not a native speaker of English and that is exactly how I write documentation in English. My comment is WRITTEN BY MYSELF and the reason why it took me 1 week to answer is that I do not know how prolog works and I spent some time working on it. :rolling_on_the_floor_laughing: :rolling_on_the_floor_laughing:

By the way, thank you for your comment on the readme. In the multivariate example I do mentioned existance of tactic can save you a lot of time. The reason why I post it there is that I want to show routine operations like "by association, by commutativity" is builtin in Litex. Litex will provide similar functionailities to tactics in the future. I put the example there because that is an example that a child might also understand, and I want more people to have a better idea of Litex (or formal language in general) .

Again, than you for your comment. Looking for your comments in the future.

[Jackie Shen]

Huỳnh Trần Khanh said:

And I don't understand what you mean by Turing complete in this context

it means Litex is not a programming language like python or lean or prolog. there is no variable, no loop, no execution in Litex. Think of Litex as a very fancy version of "ctrl+f" on your windows computer.

[Jackie Shen]

Niels Voss said:

Huỳnh Trần Khanh said:

I can smell a LLM from a distance... Sorry but I'm kinda tired of people using LLMs to churn out boring looking posts

I think this is a bit unfair. The points about facts being false vs unknown by default actually seems quite important, and the comparison is overall very useful. That being said, I do agree some of the comparisons in the readme feel a bit unfair (for example, Lean does have proof search via tactics, and it does have some built-in math without requiring external libraries)

thank you Niels. More examples will exsit in the future. I am working on formalization of weil's number theory for beginners for the time being and get many interesting ideas. I hope this work will be ready for all of you soon. If you have any simple mathematical examples that you'd like to formalize, feel free to let me know so I can think about how to formalize them in Litex.

[Jackie Shen]

suhr said:

Learning Curve
Lean4: High (The prerequisites are very high even for PhD students)

In my opinion, the difficulty of leaning Lean is grossly overstated. Also it requires basically no prerequisites, only the right point of view.

Thank you suhr. Lean is definitely a great language!

[Jackie Shen]

suhr said:

Learning Curve
Lean4: High (The prerequisites are very high even for PhD students)

In my opinion, the difficulty of leaning Lean is grossly overstated. Also it requires basically no prerequisites, only the right point of view.

suhr said:

Well, that's actually a half of a problem (the programmer's half). Another half is that while the core of Lean is a few simple rules, proving things is rarely a straightforward application of them. You quickly find proving even a simple statement hopeless unless you define a bunch of lemmas, and these lemmas also might need some lemmas to prove, and so on... And then you need to skillfully combine all the lemmas you need.

And while automation can help quite a bit with that second half, it can't solve it completely.

You are right suhr. Sometimes we underestimate the difficulty of math itself when formalizing. A small piece of math could mean a long and tedious formalization. sometimes you might find a bug in your original proof this way. While lean solves this problem by providing tactics, Litex solves this by enabling the user to formalize "the gaps" as quickly as possible by its simple syntax and more importantly, abstraction is very well handled in Litex. there is no hierarchy in Litex, just as there is no such thing in math. Litex semantics of handling relationships between objects is more like interface in Go, and I am still working on it.

Again thanks for your kind comment.

[Jackie Shen]

Arthur Paulino said:

I agree that learning Lean is not an easy task, but I don't think it has anything to do with a formal degree. The "problem" is that Lean 4 is an extremely broad and wide system, in which you can do regular programming tasks, theorem proving, programming mixed with theorem proving, FFI, meta programming etc. And each use case is a world in itself.

THank you Arthur. You are absolutely true. Lean is very nice and broad language. Since Lean is Turing complete and Litex is not, what litex can do all can be done in Lean. Litex is a small domain language, only designed for "rule-based reasoning checking". This enables Litex to have tailored syntax for and only for math verification, instead of having to work on language features unrelated to verification. I notice that not all features (like variable or control flow) in a turing complate language is required in math verification. (maybe i am wrong, but my observation is that 99% of the time we do not need that. and if one day i realize they are necessary, i will introduce them to litex as language plugin)

Again, thank you for your kind comment.

[Jackie Shen]

Thank you all for your comments. I am now working on litex zulip community (https://litex.zulipchat.com), feel free to join. Also looking for your visit to https://github.com/litexlang/golitex if you want to learn more.

[Jackie Shen]

What kind of mathematical examples are you all interested in? I’d be happy to formalize some math in Litex for everyone. This might make it easier for people to learn about Litex.

[Xiyu Zhai]

suhr said:

Well, that's actually a half of a problem (the programmer's half). Another half is that while the core of Lean is a few simple rules, proving things is rarely a straightforward application of them. You quickly find proving even a simple statement hopeless unless you define a bunch of lemmas, and these lemmas also might need some lemmas to prove, and so on... And then you need to skillfully combine all the lemmas you need.

And while automation can help quite a bit with that second half, it can't solve it completely.

I can't agree more!!! This is indeed the pain point.