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.

AI Agents Can Work With Litex

The only way to get artificial intelligence to work is to do the computation in a way similar to the human brain.

– Jeff Hinton

Litex is also becoming a good target language for AI-assisted formalization. The practical loop is simple: ask an agent to solve the theorem first in ordinary mathematical language, then translate the proof plan into Litex step by step.

When a step is not formalized yet, write it as a precise know fact. Then refine each broad know into smaller and more concrete claims, reading Litex's verification output and error messages after every run. Once the proof works, ask which lines are redundant because Litex already infers them, and which repeated structures should become a claim forall or a named prop.

This workflow makes larger examples approachable for modern coding agents such as GPT-5.5 and Codex. For instance, a formalization of a bijection from N^2 to N can be developed by letting an agent read the Manual, inspect the kernel behavior through debug output, build the proof skeleton, and shrink the remaining know facts until the argument is local and concrete.

This is remarkable. If enough agents are given enough time, perhaps much less time than we expect, they can help formalize textbooks at scale. Textbooks are especially suitable because they already reveal the argument step by step. The same pattern may eventually reach frontier papers: first recover the mathematical path in ordinary language, then make each step checkable. The main limitation today is that Litex is still young, so many basic packages and standard libraries are not ready yet. In the age of AI agents, I believe these gaps can close quickly.

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

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

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

Hi, I’m Jiachen Shen, creator of Litex. I am deeply grateful to Wei Lin, Siqi Sun, Peng Sun, Zeyu Zheng, 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.