Litex: The Formal Way to Write Math as It Looks

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

Beta notice: Litex is experimental and not ready for production or mission-critical proof work. We welcome you to try it.

What is Litex?

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 language for writing mathematical proofs that look like ordinary mathematical writing. Users write math 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. Litex code 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. Reading Litex code is a pleasant experience, because you can understand it without any prior study.

Why It Feels Simple

To understand is to see connections.

– Ludwig Wittgenstein

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.

As Hardy said, "A mathematician, like a painter or poet, is a maker of patterns.", Litex expects you to recognize familiar proof patterns (equality chains, membership, subsets, witnesses, contradiction, finite case splits). The checker matches those shapes to facts and routine consequences—more like following a textbook argument than memorizing tactic or library names for each line.

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.

Proofs Explain Themselves

Make things as simple as possible, but no simpler.

– Albert Einstein

Not only does Litex aim to be the language where mathematics verifies itself, but it also 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": "AtomicFact",
  "line": 4,
  "stmt": "$p(2)",
  "verified_by":   {
    "type": "cite forall fact",
    "cite_source": {
      "line": 2,
      "source": "entry"
    },
    "cited_stmt": "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.

Starting Points

Learn the rules like a pro, so you can break them like an artist.

– Pablo Picasso

Litex is aiming at a specific target: not making formal proof look clever, but making ordinary mathematical reasoning precise enough to check without changing its shape. Welcome to explore Litex by yourself.

Resources on the official website:

Resources:

Special Thanks

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

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