Litex: A Simple Formal Language Learnable in 2 Hours

version 0.9.73-beta

Beta notice: Litex is still an experimental project for testing ideas about formalizing everyday mathematics. It is not ready for production or mission-critical proof work yet. We hope more people will look at Litex, try it and discuss the mathematical philosophy behind it.

Jiachen Shen and The Litex Team

What is Litex?

Simplicity is the ultimate sophistication.

– Leonardo da Vinci

Litex is an open-source language for writing mathematical proofs as code.

The goal is simple: if a piece of mathematics is easy to say on paper, it should also be easy to write in a computer-checkable form.

You can think of Litex as a strict mathematical notebook. You write objects such as numbers, sets, tuples, and functions. You state facts such as x = 2 or x $in R. Litex checks whether those facts follow from what is already known.

This makes Litex feel close to daily mathematical writing. You write facts in the order you want the checker to understand them.

Here is the intended feel:

This small example shows the intended feel: Litex code looks close to the mathematical steps, while the checker handles routine rewriting, arithmetic, and reuse of known facts.

Why It Stays Simple

Litex stays simple in three ways.

Set theory and basic mathematics. Litex starts from familiar things: sets, elements, numbers, functions, tuples, relations, and facts.
Many basic relationships are built in. Litex knows many small links between equality, order, membership, functions, sets, tuples, and arithmetic.
Matching and substitution reduce naming. Litex finds known facts and known forall facts by shape, then substitutes the matching objects.

For example, in Litex:

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

The assumption x = 2 becomes known inside the local proof context. Litex can find it by matching the goal, substitute 2 for x, and let builtin arithmetic close x + 1 = 3.

This is also why forall is central in Litex. A known forall theorem is like knowing infinitely many concrete facts at once: whenever the arguments match and the assumptions hold, Litex can substitute concrete objects and use the result.

When thinking in Litex, start with three blocks: objects, facts, and statements.

Objects are the mathematical things being discussed, such as 2, R, (x, y), or a function.
Facts are claims about objects, such as x = 2, x $in R, or 0 <= x.
Statements are actions in the proof script: define an object, introduce a fact, prove a fact, or store known information.

For a deeper explanation, read the Manual, especially the Proof Process.

Proofs Explain Themselves

Litex does not only say whether a fact passed. Its output tells you how the fact was proved.

abstract_prop p(x)
know forall x R:
    $p(x)
$p(2)

The output message is like this:

{
  "result": "success",
  "type": "Fact",
  "line": 4,
  "stmt": "$p(2)",
  "verified_by":   {
    "type": "known_fact",
    "line": 2,
    "source": "entry",
    "cited_fact": "forall x R:\n    $p(x)"
  },
  "infer_facts": [],
  "inside_results": []
}

This output says that $p(2) was proved by reusing the known forall fact. Litex matched x with 2, substituted it into $p(x), and closed the goal. This makes the proof process learnable: you can see whether a fact closed by a builtin rule, a known fact, a known forall, or an inferred consequence.

Start Here

Special Thanks

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

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