Truth is ever to be found in simplicity, and not in the multiplicity and confusion of things.

– Isaac Newton

Litex is an open-source formal mathematical language for writing checked mathematical proof code. The basic loop is small:

1. Write the next mathematical fact.
2. Let Litex check it against the facts already in context.
3. Reuse the verified fact on later lines.

Here is a first proof:

forall x R:
    x = 2
    =>:
        x + 1 = 3
        x^2 = 4

Read it as ordinary mathematics: for every real number x, if x = 2, then x + 1 = 3 and x^2 = 4. Litex checks the two conclusions by using the assumption x = 2, routine rewriting, and arithmetic.

This is the central idea of Litex: users write facts; Litex grows a verified context. A Litex file introduces objects, states facts about them, checks which facts follow, stores the accepted ones, and makes them available to the lines that come after.

Litex is not intended to replace any other proof assistant. It explores a different path in formal mathematics: whether a readable, fact-oriented interface can make it easier for AI systems and humans to translate natural-language problems and textbook theorems into checkable formal proof attempts. The goal is to make ordinary mathematical reasoning precise enough for machine feedback while preserving the structure and appearance of mathematical reasoning itself.

We want Litex to become a first language for learning formalization: readable enough that even a curious ten-year-old can follow the core idea. Before learning a mature formal system such as Lean, Coq, or Isabelle, a learner can use Litex to get the basic feeling of formalization: state a mathematical fact, ask the checker whether it follows, read the output, and grow a verified context one line at a time.

Because Litex output supports multiple languages (简体中文, 繁體中文, 日本語, English, 한국어, Español, Français, Deutsch, Português, Русский, العربية, हिन्दी, Tiếng Việt, and Bahasa Indonesia), learners can write the same Litex code while reading what each line does in a language they are comfortable with, and gradually feel the appeal of mathematics and formalization. Aliases can also give local-language names to English or standard-library-facing theorem names, for example alias thm 自反等式 <=> self_eq_en, so a learner can try the formal shape before moving on to Lean-style library names.

Mathematics is a game played according to certain simple rules with meaningless marks on papers.

– David Hilbert

Think of a Litex file as a small mathematical world that grows one checked fact at a time. You introduce the objects in the world, give yourself vocabulary, state the local assumptions of the problem, and then ask Litex whether a new fact follows.

A classical syllogism shows the shape:

have human nonempty_set, Socrates human
abstract_prop mortal(x)

forall:
    forall x human:
        $mortal(x)
    =>:
        $mortal(Socrates)

This says: Socrates is human; if every human is mortal, then Socrates is mortal. The general rule is kept inside the forall premise instead of being injected into the global context.

The four moves are the basic Litex loop:

1. have human nonempty_set, Socrates human builds a tiny world.
2. abstract_prop mortal(x) adds a new word that can be used in facts.
3. The inner forall x human: ... states the local rule for this proof.
4. $mortal(Socrates) asks Litex to verify the particular conclusion.

The example is intentionally small, but it still keeps the assumption visible: Litex checks that the conclusion follows from the local premise and the rest of the context; it does not prove the premise from nothing.

When Litex accepts that final line, the verifier output can explain the route it found. The exact JSON may include line numbers and more trace fields, but the important shape is:

{
  "result": "success",
  "type": "universal fact",
  "line": 4,
  "statement": "forall :\n    forall x human:\n        $mortal(x)\n =>:\n        $mortal(Socrates)",
  "conclusions": [
    {
      "statement": "$mortal(Socrates)",
      "verification": {
        "type": "cite forall fact",
        "cite_source": {
          "line": 5
        },
        "cited_statement": "forall x human:\n    $mortal(x)"
      }
    }
  ],
  "store_facts": [
    {
      "fact": "forall :\n    forall x human:\n        $mortal(x)\n=>:\n        $mortal(Socrates)",
      "reason": "proved statement"
    }
  ]
}

The useful part is not only that a line succeeds. The output tells you whether the route was arithmetic, a known fact, a matching forall, or an inferred consequence. That makes Litex a feedback loop: write the next fact, run the checker, read what happened, and add the next piece of context.

Litex supports localized output in many languages.

{
  "结果": "成功",
  "类型": "全称事实",
  "行": 4,
  "语句": "forall :\n    forall x human:\n        $mortal(x)\n    =>:\n        $mortal(Socrates)",
  "结论": [
    {
      "语句": "$mortal(Socrates)",
      "验证": {
        "类型": "引用 forall 事实",
        "引用来源": {
          "行": 5
        },
        "被引用语句": "forall x human:\n    $mortal(x)"
      }
    }
  ],
  "存储事实": [
    {
      "事实": "forall :\n    forall x human:\n        $mortal(x)\n=>:\n        $mortal(Socrates)",
      "原因": "已证明语句"
    }
  ]
}

For most factual statements, the proof route is reported under verification. More structured facts can include a steps array inside that object. A successful forall fact instead reports conclusions, where each conclusion carries its own verification; detail output additionally expands the local parameters and assumptions. Non-factual statements such as definitions, claim, thm, and by cases report their context changes under effects; detail output can expand their local inside_results.

Every factual statement has exactly one of three outcomes: true, unknown, or error. true means Litex found a proof path relative to the current context, such as a builtin rule, a checked fact, or an explicitly stated local assumption. unknown means the statement is meaningful, but Litex did not find enough verified or assumed information to prove it. error means the line cannot be checked as a valid fact, often because the syntax is wrong or some object is not well-defined, such as an undeclared name, a function argument outside its domain, or 1 / 0.

A mathematician, like a painter or poet, is a maker of patterns. If his patterns are more permanent than theirs, it is because they are made with ideas.

– G. H. Hardy

Litex supports two complementary ways to verify a fact.

The explicit route is by thm: give a theorem a name, remember that name, and cite it with the required arguments. This is closer to the named-theorem style used by Lean and other formal proof systems.

thm add_one_after_two:
    prove:
        forall x R:
            x = 2
            =>:
                x + 1 = 3
    x + 1 = 2 + 1 = 3

by thm add_one_after_two(2)
2 + 1 = 3

The Lean shape is similar: keep a universal fact under a name, then apply that name to the object you need.

variable (Human : Type)
variable (Socrates : Human)
variable (mortal : Human -> Prop)
variable (all_humans_are_mortal : forall x : Human, mortal x)

example : mortal Socrates := by
  exact all_humans_are_mortal Socrates

The Litex-native route is pattern matching against the verified context. Instead of naming and citing the theorem, you can leave the universal fact in context and write the conclusion directly:

have human nonempty_set, Socrates human
abstract_prop mortal(x)

forall:
    forall x human:
        $mortal(x)
    =>:
        $mortal(Socrates)

Here Litex matches $mortal(Socrates) against the known forall, checks that Socrates human is already in context, substitutes x with Socrates, and verifies the conclusion. This is the core difference in proof style: Litex can use named theorem calls when names make the proof clearer, but it also lets ordinary factual lines drive verification by their mathematical shape.

The examples above are deliberately tiny. The samples below give a fast visual sense of the larger Litex surface. They are excerpts, not full runnable files; the linked pages contain runnable examples and fuller context.

The infinite-primes case study ends with the usual Euclid move: take a prime divisor of 1 * 2 * ... * a + 1, split on whether it is already below a, derive the modular contradiction, and return the larger prime as a witness.

claim forall! a N_pos: 2 <= a => exist k N_pos st {k > a, $prime(k)}:
    2 <= a <= product(1, a, '(x N_pos) N_pos {x}) <= product(1, a, '(x N_pos) N_pos {x}) + 1
    have by exist k N_pos st {$prime(k), (product(1, a, '(x N_pos) N_pos {x}) + 1) % k = 0}: k
    by cases k > a:
        case k <= a:
            product(1, a, '(x N_pos) N_pos {x}) % k = 0
            (product(1, a, '(x N_pos) N_pos {x}) + 1) % k = (product(1, a, '(x N_pos) N_pos {x}) % k + 1 % k) % k = 1
            impossible (product(1, a, '(x N_pos) N_pos {x}) + 1) % k = 0
        case k > a:
            do_nothing
    witness exist k N_pos st {k > a, $prime(k)} from k

Mathematical structures can be defined directly, with operations and axioms kept close to the ordinary textbook shape:

prop GroupProperty(s nonempty_set, inv fn(x s) s, op fn(x, y s) s, e s):
    forall x, y, z s:
        op(x, op(y, z)) = op(op(x, y), z)
    forall x s:
        op(e, x) = x
        op(x, e) = x
    forall x s:
        op(x, inv(x)) = e
        op(inv(x), x) = e

struct Group<s nonempty_set>:
    inv fn(x s) s
    op fn(x, y s) s
    e s
    <=>:
        $GroupProperty(s, inv, op, e)

Templates let users make reusable mathematical interfaces for parameterized families of sets. Ordinary tuple products can be written with cart(A, B, C); the example below uses the same Cartesian idea in a constrained function-space presentation. For any three sets A, B, and C, it names the set of three-indexed functions whose first component lies in A, second in B, and third in C, then recovers those component membership facts from the definition. The point is not that this one object is special, but that templates are useful for "for any sets of this shape" interfaces, which appear throughout mathematics.

template<A, B, C set>:
    have cart3 set = {f fn(i N_pos: i <= 3) union(A, union(B, C)): f(1) $in A and f(2) $in B and f(3) $in C}

forall g \cart3<R, Q, Z>:
    g(1) $in R
    g(2) $in Q
    g(3) $in Z

by contra, by cases, by for, by induc, by extension, by zorn_lemma are builtin statements that prove by contradiction, cases, for, induction, extension and Zorn's lemma respectively. Here by contra proves that the square function is not surjective by finding a counterexample.

prop surjective_fn(S, T set, f fn(x S) T):
    forall y T:
        exist x S st {y = f(x)}

have fn square(x R) R = x^2
forall x R:
    square(x) = x^2

by contra not $surjective_fn(R, R, square):
    have by exist x R st {-1 = square(x)}: x
    0 <= x^2
    -1 = square(x) = x^2
    0 <= -1
    impossible 0 <= -1

Visit online textbook for more examples: https://litexlang.com/doc/The_Mechanics_of_Litex_Proof/Introduction .

We are not trying to meet some abstract production quota of definitions, theorems and proofs. The measure of success of our success is whether what we do enables people to understand and think more clearly and effectively about math.

- William Thurston

Litex is experimental, but it is aiming at three simple things:

1. Human-in-the-Loop AI for Mathematical Exploration As AI makes mathematical generation abundant, Litex helps turn fragmented reasoning into scalable, verifiable, and reusable mathematical knowledge, scale users' ability to use AI for mathematical exploration.
2. Support scientific discovery. Provide an accessible, scalable framework that enables both experts and non-experts to verify, refine, and reuse mathematical reasoning across science, engineering, and AI.
3. A formal mathematical language that inspires everyone. Formal math should be a usable, readable medium for learning, communication, and research, close enough to everyday math that students, mathematicians, AI agents, and curious readers can benefit from rigor without losing sight of the ideas.

This educational goal matters for dependencies. A student learning calculus does not first memorize a huge theorem dictionary and then cite a synonym of the theorem in the book. They build definitions, lemmas, and proof habits in order. Litex's builtins provide the basic mathematical ground so that this kind of step-by-step development can start early, while larger imports and know assumptions should remain visible background, not a way to erase the book's proof. The code should be where the mathematical work happens, not only a bibliographic reference into a theorem database.

This route comes with a clear audit obligation. A Litex result should be read relative to its trusted background: builtin rules, inference rules, standard-library facts, and any explicit know assumption injections. The project goal is not to hide that boundary; it is to make the boundary visible while keeping the user-facing proof script close to ordinary mathematical writing.

For a textual walkthrough of the implementation pipeline, see Architecture. The diagram below gives the broader component landscape:

Litex kernel: the core components and their relationships.

Litex keeps the public documentation small:

1. Setup: Download Litex: install Litex, run files, and understand CLI output.
2. Manual: the source of truth for syntax, statements, proof flow, builtin rules, and inference.
3. FAQ: design rationale, trust boundaries, comparison notes, and old overview material in condensed form.
4. Litex vs Lean: dedicated comparison with Lean's interface and ecosystem.
5. Hugging Face: Litex code examples and datasets

Contact us:

1. Email
2. Zulip community

未来没有计划，但一定更好。

- 樊振东在巴黎奥运会后接受采访时说

Litex Mascot: Little Little O, a curious baby bird full of wonder

The path of Litex is a deliberate trade-off. Litex accepts a larger trusted implementation than small-kernel systems in order to make the proof surface lighter. The system tries to do more routine checking in the verifier so users can spend more of their attention on the mathematical sequence of facts. This uniqueness is the core value of Litex as a proof assistant, but it also makes contribution to Litex more difficult and demanding. We welcome young talents to try Litex and contribute to it.

Hi, I’m Jiachen Shen, creator of Litex. I am deeply grateful to Wei Lin, Siqi Sun, Peng Sun, Siqi Guo, Chenxuan Huang, Yan Lu, Sheng Xu, Zhaoxuan Hong, Xiuyuan Lu, and Yunwen Guo for their support and advice. I am sure this list will keep growing.