Litex: The Formal Way to Write Math as It Looks

by Jiachen Shen and The Litex Team, version 0.9.87-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. Litex code is intended to be readable before learning tactic names or library conventions.

Litex is not trying to be a faster Lean. It chooses a different proof interface: for textbook-style mathematics, the user writes a sequence of checkable facts, and the checker uses context plus builtin relationships to keep the feedback loop short. In a local run, more than 240 runnable examples from The Mechanics of Litex Proof checked in about 13 seconds.

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.

Litex expects you to recognize familiar proof patterns: equality chains, membership claims, subsets, witnesses, contradiction, finite case splits, and induction. 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)

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.

The output looks like

{
  "result": "success",
  "type": "AtomicFact",
  "line": 7,
  "stmt": "$mortal(Socrates)",
  "verified_by": {
    "type": "cite forall fact",
    "cite_source": {
      "line": 4
    },
    "cited_stmt": "forall x human:\n    $mortal(~1x)"
  },
  "infer_facts": [],
  "inside_results": []
}

The useful part is not only that the line succeeds. The output says $mortal(Socrates) was proved by reusing the known forall: Litex matched x with Socrates, checked the required membership fact, substituted into $mortal(x), and closed the goal. This is the explanatory surface Litex tries to provide: you can see whether a fact closed by a builtin rule, a known fact, a known forall, or an inferred consequence.

Every factual statement has exactly one of three outcomes: true, unknown, or error. true means Litex found a proof path, such as a builtin rule, a known fact, or a known forall fact. unknown means the statement is meaningful, but Litex did not find enough verified 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.

Another special design of Litex is that much of its surface vocabulary is primitive. Forms such as R, N, $in, fn, {}, and finite sets are not first unfolded into user-visible foundations; their meaning comes from the web of builtin rules, known facts, and inference rules connected to them. The keyword abstract_prop aligns with the idea that sometimes you want to use a predicate symbol without defining it yet.

AI Agents Can Work With Litex

Litex is designed so that modern coding agents can formalize textbook-style mathematics by iterating against verifier feedback. An agent can sketch a proof in ordinary mathematical language, translate it into Litex step by step, run the checker, read why each fact failed or succeeded, and refine the argument until every step is local and concrete.

A concrete example is the final example in Chapter 8, which proves that there is a bijection from N^2 to N using Cantor pairing. Codex formalized this example in Litex by reading the Litex manual and verifier output, then iteratively refining the proof until it became fully checkable, without relying on an external mathematical library. This is mainly evidence that the Litex proof style exposes a useful feedback loop, not a claim that the theorem itself is difficult for mature proof assistants.

This is the point Litex is trying to make especially strong: Litex gives agents a direct debugging surface. The agent states the next mathematical fact, runs the checker, reads the local success or failure, and continues in the same language as the proof. Litex is still early, but this feedback loop is a practical way to discover which background facts and theorem-library entries a proof actually needs.

Starting Points

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.

For different readers:

Soundness and Limitations: for readers who care about the trusted base, know, builtin rules, and current limitations.
Research Positioning: for proof assistant researchers and formal mathematics readers.
AI Agent Workflow: for AI and formal math work using verifier feedback.
Benchmarks and Case Studies: for reproducible examples and future evaluation.
AI for Science: for local verification of scientific and applied mathematical derivations.
Litex 中文战略一页纸: for Chinese strategic and project discussions.
Outreach Guide: for contributors writing emails, posts, and audience-specific pitches.

Resources on the official website:

Resources:

Special Thanks

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

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