Litex: Write math the way it looks

by Jiachen Shen and The Litex Team, version 0.9.73-beta

Beta notice: Litex is experimental and not ready for production or mission-critical proof work. We welcome people to try it and discuss the mathematical philosophy behind it.

What is Litex?

Simplicity is the ultimate sophistication.

– Leonardo da Vinci

Litex is an open-source language for writing mathematical proofs that look like ordinary mathematical writing. Users write facts almost exactly as they would in notes or textbooks; Litex checks them, stores verified results, and lets the proof grow from the context.

The central idea is: users write facts; Litex grows a verified context. A file introduces objects, states facts, checks them, stores successful ones, and reuses them later.

Litex is designed around ordinary mathematical writing: objects such as numbers, sets, and functions; facts such as x = 2 or x $in R; and statements that grow a proof step by step.

It emphasizes a set-theoretic surface, proof scripts as verifiable facts, a growing context, and proof output that explains why each fact was accepted.

Here is the intended feel:

This shows the intended feel: Litex states the desired facts directly, while the checker handles routine rewriting, arithmetic, and reuse of known facts.

Why It Feels Simple

Litex feels simple because routine mathematical structure lives in the checker, not in user proof scripts.

Facts are proof steps. A script mostly states mathematical facts in reading order.
The context grows. Once verified, a fact is stored and can produce routine consequences.
Basic mathematics is built in. Litex knows small links between equality, order, membership, functions, sets, tuples, and arithmetic.
Statement shapes guide matching. Litex matches known facts and forall facts by shape, then substitutes the matching objects.

In this sense, Litex aims to be the language where mathematics verifies itself.

For example, a syllogism is ordinary mathematical information:

have human nonempty_set, Socrates human
abstract_prop mortal(x)

know forall x human:
    $mortal(x)

$mortal(Socrates)

The user does not say "apply the theorem with x = Socrates." Litex matches $mortal(Socrates) with the known forall, sees that Socrates belongs to human, and verifies the conclusion.

This is why forall is central: a known forall theorem acts like infinitely many concrete facts, ready to use when arguments and assumptions match.

Think in three blocks: objects, facts, and statements.

Objects are mathematical things: 2, R, 'R(z){z}, {1, 2, 3}, or 1 + 2.
Facts are claims about objects: x = 2, x $in R, 0 <= x, forall! x set => {x = x}, or exist x R st {x ^ 2 = 4}.
Statements are proof-script actions: define an object, introduce a fact, prove a fact, or store known information.

For more, read the Manual, especially Proof Process.

Proofs Explain Themselves

Litex does not only say whether a fact passed. It tells you how it was proved.

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

The output looks like:

{
  "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 says $p(2) was proved by reusing the known forall: Litex matched x with 2, substituted into $p(x), and closed the goal. 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

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

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