Litex: A simple formal language which 10-year-olds learns quickly

Simplicity is the ultimate sophistication.

-- Leonardo da Vinci

Litex is an ambitious project with a clear vision: to create a simple, intuitive, and powerful formal language for mathematics. The goal of Litex is to scale reasoning at this AI era by making it more accessible to everyone. If a 10-year-old can intuitively grasp logical reasoning for simple math proofs, a formal language should be just as intuitive and accessible. Litex aims to be that human-friendly language -- making formal language simple enough for anyone to learn and use.

World-class researchers including Terrence Tao, Yoshua Bengio, and AI companies including DeepMind and DeepSeek, are showing great interest how formal languages can be used to scale reasoning AI, ensure AI safety, and many more tasks. Litex is the perfect tool to their challenge. Litex has already gained attention from leading institutions worldwide, including CMU, Mila, Tsinghua, PKU, ByteDance, OpenMMLab, SJTU, Fudan.

Learn more in tutorial. Download the latest version of Litex here. Try Litex in your browser here.

While Litex is in the early stages of development, it has already established a solid foundation that demonstrates the potential of this approach. Contributors read contribute to Litex for more details. If you have any problems, please contact us through Contact methods provided in this README.

NOTE: Litex is still under development. THE CREATOR OF LITEX IS LOOKING FOR LONG-TERM OR SHORT-TERM CONTRIBUTORS. READ CONTRIBUTE TO LITEX FOR MORE DETAILS.

WARNING: Litex is still under development. Unexpected bugs might happen.

This section is for you to try Litex step by step. If you just want to have a quick look at Litex, you can skip this section.

Visit Litex Playground to try Litex in your browser.

step 1: download latest version release. It is a binary file, so you can just run it in your terminal.

step 2: run your downloaded binary file and enter the REPL (Read-Eval-Print Loop) mode of Litex. Try enter 1 + 1 = 2 and see what happens. Enter exit to quit the REPL mode.

If you are on Mac, you might need to give it permission to run. If it still does not work, input chmod 777 YOUR_BINARY_FILE_NAME in your terminal and try again.

step 3: git clone https://github.com/litexlang/golitex.git and run YOUR_BINARY_FILE_NAME PATH_TO_YOUR_CLONED_REPO/examples/comprehensive_examples/syllogism.lix in the root directory of the cloned repo. This will run the example code. Other examples (e.g. Hilbert geometry axioms formalization for experts, multivariate linear equation for children) are in the same directory. You can also input the code directly in the REPL mode.

Both choices are free. I recommend you to try Litex in your browser first, because it is much more convenient.

SORRY THERE IS NO MORE EXAMPLES FOR NOW. I SINGLE-HANDEDLY DEVELOPED THE WHOLE LANGUAGE FOR 2800 GIT COMMITS. I HAVE ALREADY DONE MY BEST. THAT IS WHY I AM SO EXCITED TO HAVE YOU HERE.

After having a sense of Litex, do this:

0. Read the README to get a sense of the project.
1. Read the tutorial to get a sense of the language.
2. Read the comparison with Lean to get a sense of the difference between Litex and Lean.
3. To learn applications of Litex, read applications of formal reasoning in AI and many other fields.
4. To read a comprehensive example, read formalization of Hilbert geometry axioms.
5. Contribute piece by piece to the Litex kernel or the Litex dataset, e.g. formalize mathematical concepts, fix bugs, add new features, improve documentation, etc. on github, discord.

IF YOU HAVE ANY PROBLEMS, PLEASE CONTACT THROUGH discord OR [email protected] OR github.

THANK YOU FOR YOUR FEARLESS EARLY ADOPTION! HERE IS MY HEARTFELT THANKS TO Litex's EARLIEST FANS -- THE BOLD PIONEERS WHO TRUSTS ME FROM THE START!

If you define the problem correctly, you almost have the solution.

-- Steve Jobs

Mathematics is the art of deriving new facts from established ones. To illustrate, consider a classical syllogism proposed by Aristotle, which formalizes deductive reasoning as follows:

Litex Lean 4

set Human prop self_aware(x Human) know forall x Human:     $self_aware(x) obj Bob Human $self_aware(Bob)	def Human := Type def self_aware (x : Human) : Prop := true axiom self_aware_all :     ∀ (x : Human), self_aware x example (Bob : Human) : self_aware Bob := self_aware_all Bob

Consider Human as the set of all humans. Using know, we establish a simple fact: all humans are self-aware. Since Bob is in the set of Human, "Bob is self-aware" is true. This simple example shows how Litex builds math from basic pieces, like building blocks. By match and substitute, Litex verifies the correctness of the reasoning just like how you verify the correctness of your daily reasoning. Each statement in Litex has four potential outcomes: true, false, unknown, or error. All factual statements start with $ to differentiate them from functions.

Notice how Litex is much simpler than Lean4. Instead of writing complex axioms with special names, you just use familiar words like know and forall. Litex automatically finds the facts it needs, just like searching in a database. Moreover, there are less unfamiliar keywords, less twisted syntax in Litex. People can understand Litex at first glance and say "oh, I already get this." instead of trying to figure out what this keyword or that syntax means. Users can focus more on math itself instead of the formal language they use. Litex's syntax is similar to Python and Go, so if you've done any programming, you'll feel right at home. See more in comparison with Lean, tutorial.

Keep it simple, stupid.

-- The Unix Philosophy

There are two things in math: objects and factual statements. Objects are the things that we are talking about, and factual statements are the statements about objects. Sets, functions, numbers, etc. are all objects. And factual statements are statements like "Jordan is intelligent", "1 < 2", "x = 1", etc. In Litex, a factual statement has four potential outcomes: true, false, unknown(not enough information to determine the truth value), or error(the statement is not well-formed). A fact is a statement that is true.

Math is built on top of a small sets of reasoning rules and axioms. There are basically two types of deriving a new fact from existing facts:

1. derive from a specific fact: e.g. If I know x = 1, then x = 1
2. derive from a general fact: e.g. If I know forall human, he is intelligent, and Jordan is a human, then Jordan is intelligent. Litex calls this way of deriving a new fact "match and substitute", because it is like matching a pattern and substituting the pattern with a specific value.

Amazingly, with these two ways of deriving a new fact, and with a set of carefully chosen axioms, we can (nearly) build the entire world of mathematics. And you have ALREADY learned the basic mechanism of Litex in just one minute: match and substitute. Pretty simple, right?

All daily math is built around first-order-logic, naive set theory, natural numbers related axioms (mathematical induction, Peano axioms, extension to rational numbers and real numbers), and all of these are implemented in Litex. So it does not matter whether you are formalizing algebra or geometry or any other math, as long as you are clear about concepts and axioms of the math you are formalizing, you can use Litex to formalize it.

A major special case of match and substitute is about rational numbers, like 1, 3.5 or 4.123456789. These objects are different from user-defined objects because their literal representation directly encodes information. Rational numbers and their basic operations like addition, multiplication, inequalities are builtin in Litex, and Litex handles all the verification rules for them automatically.

Common sense is not so common.

-- Voltaire

Everyone knows how to reason, including 10-year-old. We reason thousands of time every day without even noticing it. Yet, traditional formal languages, like Lean4, Coq, and Isebelle are so complex that even the smartest mathematicians find it hard to use. Why is that?

It turns out that these languages attempt to serve two distinct purposes simultaneously: they want to be both programming languages and reasoning verifiers. This dual nature makes it technically challenging to create a simple and intuitive system. These languages heavily rely on type theory and functional programming concepts, which even mathematics PhD students need years to master.

If Newton had to learn those theories before inventing calculus, he would never succeed, because those theories would be invented 3 centuries later.

On the other hand, Litex is a formal language that operates as a Read-Only Turing Machine. By deliberately sacrificing Turing completeness, Litex focuses solely on mathematical verification. Unlike programming languages, Litex eliminates variables, control flow, and execution semantics - concepts that are foreign to pure mathematics.

This design choice, similar to how SQL specializes in database operations, allows Litex to specialize in everyday math as much as possible. The language adopts Python-like syntax for accessibility.

Another important design choice is that the user does not need to give names to facts, because Litex can automatically find the matched facts it needs. It saves a lot of time and effort for the user. Read tutorial for more details.

Throughout the years, natural languages are considerably more expressive than their formal mathematical counterparts. With Litex, we can finally make the best of both worlds.

In a nutshell, Litex is for EVERYONE, from children to experts, to learn and use formal language at AI age. It scales up reasoning by making the process of writing formal reasoning as intuitive as writing in natural language.

This is a summary of the differences between Litex and Lean4.

Feature Litex Lean4

Turing-complete	❌ No	✅ Yes
Focus	Math formalization	Proof + Programming
Syntax Style	Python-like	Functional
Learning Curve	Low (10-year-old friendly)	High (The prerequisites are very high even for PhD students)
Auto-fact Finding	✅ Yes (automatic)	❌ No (manual naming)
Type System	Set theory + first-order logic	Complex (dependent types)
Built-in Math	✅ Yes (rational numbers, basic operations)	❌ No (requires libraries)
Community Size	Small (growing)	Large (established)
Production Ready	❌ Not yet	✅ Yes

1. Why is Litex poised for success now?

Litex represents an intellectual breakthrough in formal language design. The rapidly expanding AI industry presents the perfect opportunity, as it needs tools for ensuring AI safety, enhancing reasoning, and accelerating scientific discovery.

2. What makes Litex different from other formal languages?

Litex's greatest strength is its remarkable simplicity. While other formal languages require years of expertise to master, Litex is intuitive enough for children to learn, striking the perfect balance between power and accessibility.

3. How do I formalize concepts like uniform distribution over (0,1) or anything like that?

Think of formalization like reading a book - you need to understand the previous pages before the last one. Similarly, formalizing advanced concepts requires building up from fundamentals. For example, formalizing uniform distribution over (0,1) requires many prerequisites. The good news is that translating mathematical concepts to Litex is straightforward once you have the prerequisites in place.

4. Resources of Litex:

Applications of Formal Reasoning in AI and Many Other Fields

Tutorial

Formalization of Hilbert Geometry Axioms

Compare Litex with Lean

Website

Github

If I have seen further, it is by standing on the shoulders of giants.

-- Isaac Newton

Here are some examples of Litex, in comparison with Lean4. Detailed explanations are provided in comparison with Lean. I put them here for you to get a sense of the language.

The definition of algorithm is a good example. In mathematics, an algorithm is a computational method that can be precisely defined as a quadruple (Q, I, S, f), where:

• Q is a set representing all possible states of computation
• I is a subset of Q representing valid inputs
• S is a subset of Q representing valid outputs
• f is a function from Q to Q that defines the computational rule

The computation proceeds by repeatedly applying f to an input x in I, generating a sequence x₀, x₁, x₂, ... where x₀ = x and xₖ₊₁ = f(xₖ). An algorithm must terminate in finitely many steps for any valid input, producing an output in S. This formal definition ensures that algorithms are well-defined mathematical objects that can be rigorously analyzed and verified.

Litex Lean 4

fn comp_seq(Q set, f fn(Q)Q) fn(Q, N)Q:   forall x Q:     comp_seq(Q, f)(x,n) = f(comp_seq(Q, f)(x, n-1)) exist_prop n N st exist_comp_seq_end(Q set, x Q, f fn(Q,N)Q):     f(x, n) = f(x, n+1) prop is_algorithm(Q set, I set, f fn(Q)Q):   $subset_of(I, Q)   iff:     forall x I:         $exist_comp_seq_end(Q, x, comp_seq(Q, f))

structure ComputationalMethod where   Q : Type   I : Set Q   S : Set Q   f : Q → Q   f_fixed : ∀ q ∈ S, f q = q namespace ComputationalMethod def comp_seq (cm : ComputationalMethod) (x : cm.Q) : ℕ → cm.Q   | 0 => x   | n + 1 => cm.f (comp_seq x n) def TerminatesIn (cm : ComputationalMethod) (x : cm.Q) (k : ℕ) : Prop :=   comp_seq cm x k ∈ cm.S ∧   ∀ i < k, comp_seq cm x i ∉ cm.S def IsAlgorithm (cm : ComputationalMethod) : Prop :=   ∀ x ∈ cm.I, ∃ k, TerminatesIn cm x k end ComputationalMethod

Next I want to show you how Litex can be used to solve a simple linear equation. It's clear that the Litex version can be read and understood by a 10-year-old, while the Lean version is much more complex.

Litex Lean 4

obj x R, y R:   2 * x + 3 * y = 10   4 * x + 5 * y = 14 2 * (2 * x + 3 * y) = 2 * 10 4* x + 6 * y = 2 * 10 (4*x + 6 * y) - (4*x + 5 * y) = 2 * 10 - 14 (4*x + 6 * y) - (4*x + 5 * y) = y y = 6 2 * x + 3 * 6 = 10 2 * x + 18 - 18 = 10 - 18 2 * x + 18 - 18 = -8 (2 * x) / 2 = -8 / 2 (2 * x) / 2 = x x = -4

import Mathlib.Tactic example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by   have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁]   have h₄ : 4 * x + 6 * y = 20 := by linear_combination 2 * h₁   have h₅ : (4 * x + 6 * y) - (4 * x + 5 * y) = 20 - 14 := by     rw [h₄, h₂]   have h₆ : (4 * x + 6 * y) - (4 * x + 5 * y) = y := by     ring   have h₇ : 20 - 14 = 6 := by norm_num   have h₈ : y = 6 := by     rw [←h₆, h₅, h₇]   have h₉ : 2 * x + 3 * 6 = 10 := by rw [h₈, h₁]   have h₁₀ : 2 * x + 18 = 10 := by     rw [mul_add] at h₉     simp at h₉     exact h₉   have h₁₁ : 2 * x = -8 := by     linear_combination h₁₀ - 18   have h₁₂ : x = -4 := by     linear_combination h₁₁ / 2   exact ⟨h₁₂, h₈⟩

I know Lean can use tactics to solve the same problem, and it is shorter. Litex will introduce similar features in the future. What I really want to show you here is that Litex is much more readable and intuitive than Lean in this case. Not every situation can be solved by tactics, and writing tactics itself in Lean is not easy. Litex spares you from remembering all these difficult things like have, by, rw, simp, exact and strange syntax etc. All you need is basic math knowledge, which significantly reduces the barrier to entry.

The best way to predict the future is to invent it.

-- Alan Kay

Hi, I am Jiachen Shen, the creator of Litex. I am a PhD student in mathematics and programming language enthusiast (a programming language geek, if you are one too, you are welcome to contact me). In 2023, I shockingly found that math is somehow equivalent to programming, after reading Professor Terence Tao's blog. This is the most amazing idea that I have ever seen in my life. In 2024, after thinking about it for a year, I started to implement Litex. After more than 2500 git commits, what it means to be a "formal language that is intuitive and as aligned with daily math expression as possible" is finally to make sense to me and my kernel sort of works now.

Litex is evolving from implementation to community-driven development. The interpreter is 90% complete and covers most daily math. However, it is still not ready for production use. Now, I face a big challenge: the conflict between an individual's limited capacity and the extensive demands of an open-source project. See more in contribute to Litex to help me grow the project.

You can contribute by:

1. Contributing to the interpreter or standard library
2. Creating datasets for AI training
3. Improving documentation
4. Exploring Litex's mathematical capabilities
5. Spreading the word about Litex
6. Building standard library of Litex
7. Creating the LitexDojo, similar to how LeanDojo is for Lean.

Since 90% of the functionality delivered now is better than 100% of it delivered never¹, the inventor of Litex put it open-source to welcome everyone, including you, to learn, try, use, and contribute to Litex, even though Litex is not fully ready. Feel free to contact us and join this exciting journey!

• Website: litexlang.org
• GitHub: github.com/litexlang/golitex
• Project Email: [email protected]
• Litex Creator: Jiachen Shen
• Litex Creator's Email: [email protected]
• Discord: discord

1. Kernighan & Plauger, The Elements of Programming Style, 1978. ↩