Litex: The Formal Language Where Math Verifies Itself

“Truth is ever to be found in simplicity, and not in the multiplicity and confusion of things.”

What is Litex?

Litex is an experimental formal language for mathematics, started in 2024. Its source expresses definitions and proofs through familiar sets, functions, and explicit mathematical facts.

Learn by examples Litex Manual Set up Litex

University

Set theory

Cantor's theorem · Sets, functions, contradiction

Cantor's diagonal argument

For any proposed function f from a set S to its power set, form the diagonal set of elements x that are not in f(x). If f reached every subset, it would reach that set at some a—forcing a to be both in and not in f(a). The whole argument is runnable and checked, with no user-written trust fence.

Loading editor…

01

Fact-oriented

Write the next mathematical fact.

The checker searches the available context for a local justification.

02

Set-theoretic

Keep mathematical objects readable.

Domains and conditions stay explicit in the source.

03

Mathematical workflow

Explore, check, keep, and reuse.

Work interactively in a Session or organize definitions and proofs in project files.

04

Human–AI feedback

Advance through explicit feedback.

Machine-readable results identify accepted steps and failed obligations.

05

Lean integration

Work toward independent rechecking.

Ongoing work on translating supported Litex proofs into Lean.

Writing mathematics in Litex

Define the objects in your problem, then state the intermediate facts that lead to your conclusion. Use the feedback to correct a step that cannot yet be checked.

Objects · small foundations

“Geometry, like arithmetic, requires for its logical development only a small number of simple, fundamental principles.”

— David Hilbert

Start with familiar sets, elements, and functions, with their mathematical conditions visible.

Relations · visible connections

To understand is to see connections.

— Ludwig WittgensteinAdapted from Philosophical Investigations, §122.

AI-assisted mathematics should deepen human understanding. Litex's JSON records why statements were accepted, the rules and premises used, and the facts cited. Tracing these dependencies helps readers see how definitions and results connect, examine assumptions, and recognize where a proof can be reused.

Formalization that follows your mathematical workflow.

Edit the Newton example below, then inspect its verification record and knowledge graph.

Define an idea

Name the objects and make their mathematical conditions explicit.

Try and check

Test concrete examples, read the feedback, and revise the next step.

Keep useful results

Accepted statements leave knowledge for later reasoning within their scope.

Reuse and communicate

Keep definitions and theorems in project modules; use results in calculations or write them up.

Loading editor…

Think, write, and check as you go.

Define a reciprocal, inspect why zero is rejected, and continue in the same Session.

Terminal REPLRecorded terminal REPL · failure diagnostic summarized

litex> have fn f(x R: x != 0) R = 1 / x
success
litex> f(2) = 1 / 2
success
litex> f(0) = 0
Failed: input 0 does not satisfy x != 0.
litex> f(4) = 1 / 4
success

Keep today's results for the next exploration.

Prove the Newton fixed-point theorem in newton.lit, then apply it to √2 from example.lit.

example.litUse the theorem from newton.lit

release obj def newton::newton_sqrt_two
release thm newton::fixed_point(sqrt(2))

View the project files · definition, proof, and configuration

newton.litPositive update and fixed-point theorem

claim:
    ? forall x R+:
        (x + 2 / x) / 2 $in R+
    2 / x > 0
    x + 2 / x > 0
    (x + 2 / x) / 2 > 0

have fn newton_sqrt_two(x R+) R+ = (x + 2 / x) / 2

thm fixed_point:
    ? forall x R+:
        x^2 = 2
        =>:
            newton_sqrt_two(x) = x
    x = x * x / x = x^2 / x = 2 / x
    newton_sqrt_two(x) = (x + 2 / x) / 2 = (x + x) / 2 = x

litex.configLoad the library before the example

[export]
newton = "./newton.lit"
example = "./example.lit"

These files form one project. The qualified theorem call is checked in that project context.

Put supported computations to work in Python or C, write up the mathematics in LaTeX, and follow the ongoing Lean integration for independent rechecking.

Read, run, and connect the results

Learn Litex See how the checker works

How Litex works

Small checking steps return explicit evidence about the rules and premises used. These records explain a result and provide a route to Lean replay.

Litex verification pipeline: a candidate fact passes through well-definedness and bounded local verification, supported by scoped knowledge and builtin rules. Success stores, infers and commits knowledge; failure preserves earlier context. The inset shows direct evidence, known properties, builtin rules, strategies, definitions and forall, and permitted rewriting. — An overview of checking an atomic fact: read the current knowledge, check that expressions are meaningful, and look for supported local grounds. Accepted facts extend the context; an unsuccessful check returns its stopping point while preserving earlier accepted knowledge.
Open original English diagram

Small steps. Clear evidence. Replayable proofs.

A long proof can consist of small, explicit checks: the goal, the rule used, and its premises. Each successful step returns this evidence to the calling step.

Each supported builtin rule records its name, arguments, and premise proofs. Mapping these local steps to checked Lean theorem applications or tactic sequences provides a route to replaying the complete proof.

The structured execution results supply the evidence for JSON explanations and Lean replay. Lean integration is ongoing; each verification route needs a faithful, checked Lean mapping.

Explore the Lean compiler Explore the kernel source Read the architecture

Explore how Litex works

“The best way to predict the future is to invent it.”

— Alan Kay

Litex Goals

Our goal is a Python for formal languages: familiar mathematical writing with a lower learning barrier.

Litex is for everyone

Knowledge we can understand and reuse.

A tool for helping more people become experts.

People should be able to read AI-generated proofs, question their assumptions, and master the mathematical tools they use.

For math learners

For students from primary and secondary school onward: explore mathematical ideas, explain why a result holds, and develop understanding and reasoning. Ten output languages and JSON feedback help you inspect the grounds behind each check while learning mathematics, formalization, and programming step by step.

For AI developers

Concise Litex syntax and structured JSON feedback are your friends: propose a mathematical step, inspect the result, and build the next proposal into your pipeline.

For mathematicians

Manual review can take a year or more; once a proof is formalized, checking its logic can take minutes. Existing formal languages often have a steep learning curve. Litex aims to lower that barrier through familiar mathematical writing, making formal tools easier to understand and master.

Understanding · Fidelity · Transparency · Review · Responsibility · Openness · Honesty

Litex aims to keep AI-assisted mathematics understandable, reviewable and accountable: source expresses mathematical intent, verification records expose grounds, and mathematical judgment and responsibility remain with people.

Litex's mathematical values →

These goals echo related principles in the Leiden Declaration on Artificial Intelligence and Mathematics.

More for mathematicians

For engineers

Turn supported, checked computational definitions into executable Python, connecting mathematical reasoning with code you can run.

“What I cannot create, I do not understand.”

— Richard Feynman

Math for AI

Give AI a language for checkable mathematical work. AI proposes; Litex checks; accepted knowledge accumulates.

Build an agent loop around one live Litex Session.

Give the agent a mathematical task, load the relevant context once, and let it propose one complete statement at a time. Verification feedback determines whether to keep the result or repair the pending statement.

Litex agent pipeline: a natural-language reciprocal problem, AI proposals, JSON feedback and repair, retained facts, a checked Litex file, and illustrative Python, dependency graph, LaTeX and Lean outputs. — One reciprocal problem, from an AI proposal through verification and repair to reusable mathematics. The output previews illustrate possible uses of the checked source.
Original English PNG Original English SVG

Human meaning

Agent proposal

Litex feedback

HUMAN MATHEMATICAL TASK

Define the reciprocal on nonzero real numbers and prove that multiplying it by its argument gives one.

01 · Load context

Understand the task and load its interfaces once.

The task asks for a reciprocal on nonzero reals. Start one terminal Session and make that domain explicit in the function definition.

First accepted definitionOne statement in the live Session

have fn reciprocal(x R: x != 0) R = 1 / x

Litex responseActual interactive success response

success

The reciprocal definition is available in this Session. The agent records this accepted source before proposing the next statement.

Accepted

Journal the source and continue from the enlarged context.

Ordinary failure

Keep the live Session, inspect the missing grounds, and repair the pending statement.

Stopped Session

Record the error, reopen the intended context, and replay the accepted prefix.

A claim and its nested proof form one statement. A multi-statement frame can partially commit: record each response before retrying. Failure is not proof of a proposition’s negation.

The terminal prints success for accepted statements and JSON diagnostics for failures. Clean file runs return JSON receipts. This recorded example illustrates the protocol; the website playground runs files separately.

What is next?

Keep the same mathematical work useful beyond the current problem: write it up, run a supported computation, and connect to other tools. LaTeX and Python outputs are available today; Lean integration is ongoing.

Litex to LaTeX.

Turn mathematical definitions, facts, and proof steps into LaTeX for papers, notes, and teaching. Here the distance-from-zero example becomes a definition, a general fact, and a concrete calculation.

LitexChecked mathematical source

have fn distance_from_zero(x R) R = abs(x)

forall x R:
    distance_from_zero(x) = abs(x) >= 0

distance_from_zero(-3) = distance_from_zero(3) = 3

Definition distance_from_zero.

Let $\mathit{distance\_from\_zero} : \mathbb{R}\to \mathbb{R}$ .

\mathit{distance\_from\_zero}\left(x\right) = \left|x\right|

For every $x\in \mathbb{R}$ , we have $\left(\mathit{distance\_from\_zero}\left(x\right) = \left|x\right| \geq 0\right)$ .

\mathit{distance\_from\_zero}\left(-3\right) = \mathit{distance\_from\_zero}\left(3\right) = 3

LaTeX renders parsed source. Proof verification is a separate step.View LaTeX conversion on GitHub

From checked mathematics to executable code.

A supported computational definition can become runnable Python. Here is the Newton update from our earlier example, with an explicit restart at zero.

LitexChecked computational definition

algo newton_step(x R) R by cases:
    case x = 0: 1
    case x != 0: (x + 2 / x) / 2

PythonGenerated by the current CLI

def newton_step(x):
    if x == 0.0:
        return 1.0
    elif x != 0.0:
        return ((x + (2.0 / x)) / 2.0)
    raise AssertionError("unreachable verified Litex cases")

Executed: 1.0 → 1.5 → 1.4166666667.

Experimental extraction for supported numeric definitions, with Python and C99 targets. Generated code uses floating-point arithmetic.View Python / C extraction on GitHub

Litex to Lean.

Ongoing

We’re developing compilation from supported Litex proofs to Lean for independent rechecking.

LitexRecorded source

1 = 1

LeanEarlier compiler output · excerpt

import Litex

theorem __fact0 : Litex.Same (1 : ℂ) (1 : ℂ) := by
  exact Litex.Same.refl (1 : ℂ)

Lean integration is ongoing. This excerpt comes from an earlier compiler experiment.View the Lean compiler project on GitHub

Mathematics textbooks, from school to university.

We plan to build a complete Litex mathematics curriculum, gradually covering primary and secondary school mathematics and core undergraduate subjects. Definitions, proofs, and worked examples will become knowledge learners can check, understand, and reuse.

Explore mathematics

A wider horizon

Beyond the Search for One Best Language

“Mathematics is the queen of the sciences.”
— Carl Friedrich Gauss

Mathematics is the mother of the natural sciences. Alongside Lean, Mizar, Isabelle, and Rocq, Litex explores a new design perspective: familiar ideas brought together around a readable, fact-oriented interface.

In tactic-oriented workflows, authors describe how to build a proof. Litex starts from what should hold and lets the verifier seek a justification in context. Such reversals of the starting assumptions guide many of its design choices.

Compare Litex and Lean through examples →

As AI helps more people use mathematics, formalization could follow it into more disciplines. Litex aims to lower the learning barrier so more people can understand and use checked mathematics in science and engineering. We believe formal mathematics has more than one possible future.

Community and support

Litex grows with its community.

Researchers, users, friends, and partner organizations help make Litex possible.

Pen sketch of Isaac Newton — — Isaac Newton

Sponsors and partners

What people say

How readers describe Litex

“From knotted cords to symbolic notation, the choice of representation has always shaped human thought. Arabic numerals and Newton's calculus notation prevailed because of their clarity and simplicity. As formal languages evolve today, Litex may likewise open new possibilities by enabling us to reason clearly, simply, and formally.”

Zeyu Zheng

PhD Candidate at CMU

“The only language capable of verifying advanced arguments using the mathematical notation familiar since elementary school.”

Yuniruyuni

Math Lover from Japan

“I appreciate a serious contender in the field of interactive theorem proving. Currently the field is dominated by Lean and Rocq, and I appreciate that Litex is challenging this duopoly.”

Huỳnh Trần Khanh

Lean Expert from Vietnam

“Litex is a hacker-built, community-driven, and highly creative project that brings value to everyone working on AI and mathematics.”

Siqi Sun

CTO of Intelligen, Research Scientist at Shanghai AI Lab and Fudan University

“I'm a happy researcher dedicated to making AI more trustworthy and protective of humanity. Litex is the formal language that can help align AI reasoning with human understanding in this big AI dream!”

Jie Fu

Yoshua Bengio's Postdoc

“Litex is much easier to use compared to other formal languages like Lean. While it is still in its infancy, I believe it has the potential to become a powerful research tool that every scientist will be able to easily use and be eager to adopt in the future.”

Yan Lu

Research Scientist at Shanghai AI Lab

With gratitude

Built in conversation.

Special thanks to Wei Lin, Siqi Sun, Peng Sun, Yi Wang, Chenxuan Huang, Yan Lu, Sheng Xu, Keyao Zhu, Xingjian Ma, and Zhaoxuan Hong for their support and advice.