# golitex makes Litex a checkable, fact-first formal language

> golitex is the Rust implementation of Litex, a formal language where you write a mathematical fact and the checker returns the grounds it found or where checking stopped, with a session mode built for AI assisted work. It suits someone who wants checkable mathematics with a shallow entry curve, and it is not a replacement for a dependent type theory.

**litexlang/golitex** — Litex: a formal language which lets machines and humans speak the same mathematical language

- Repository: https://github.com/litexlang/golitex
- Website: https://litexlang.com
- Stars: 676 · Forks: 10
- Language: Rust
- License: Apache-2.0
- Published: 2026-10-21 · Updated: 2026-10-21 · Language: en
- Canonical page: https://hysenlabs.com/projects/litexlang-golitex

## The unit of work is a fact, and the checker explains what it used

Litex is described as a formal language for everyone who wants to write and understand checkable mathematics, and the readme's framing line is that you write mathematics and see why it holds. The smallest example makes the design legible:

```text
1 + 1 = 2
have a R = 2
a + 1 = 3
```

The first line is checked by calculation. The second introduces a as a real number, and the checker records a as a member of the reals and as equal to 2. The third statement is then checked using the facts already available and stored for later steps. The important part is the division of labour. The author chooses what to establish, and Litex searches for supported local grounds and reports the method it found. That is a different contract from a proof assistant that asks you to supply a tactic or a term. The readme also sets a limit on what to expect, saying these are small examples of a fact-oriented interface and not a claim that the verifier can invent an entire proof from its final statement. The vocabulary is deliberately small. A definition introduces a proposition with a body, and applying it with a dollar sign keeps the result in the current context:

```text
prop is_odd(x Z):
    x % 2 = 1

$is_odd(3)
```

The checker verifies the concrete claim through the definition and keeps the result available. The design goal is stated as a Python-like entry into formal mathematics, where more people can learn to build checkable knowledge.

## Set theory is the substrate, so everything starts from membership

Litex takes set theory, ZFC, as its mathematical foundation, and presents sets, elements, functions and relations as the working vocabulary. The readme draws a contrast with how a typical type-theoretic author works. In a statement like have a R = 2, membership and equality are facts the language can use again, and the author does not first choose an abstract carrier type for a. The same starting set lets a file define a set, a function and a comparison, then use them:

```text
have S set = {x R: x > 0}
have fn square(x R) R = x^2
square(2) = 4

prop is_less(x, y R):
    x < y

$is_less(2, 4)
```

The readme is careful about a boundary here. Function domains, set membership and other well-definedness conditions still have to be checked before a statement is accepted, so the set-theoretic default does not mean the checker skips the obligations. It also notes that symbol input is accepted, since a symbolic intersection and subset expression is a spelling of the letter-based intersect and subset functions, and that most examples use the letter-based spelling because it is easier to type on an ordinary keyboard. The comparison with Lean in the readme is careful and worth repeating, since it says the comparison is between their default interfaces and not their current coverage. Lean elaborates proofs into a core dependent type theory, while Litex makes set membership and facts the default authoring layer.

## Accepted facts accumulate, and a claim asks for a witness

The growth model is that every accepted statement extends the mathematical context for the statements that follow, and the longer example shows a quantified claim being discharged against a witness rather than proved from first principles:

```text
prop is_positive(n R):
    exist a R+ st {n > a}

claim:
    ? forall x R:
        x > 10
        =>:
            $is_positive(x)
    witness exist a R+ st {x > a} from 10

have a R:
    a > 10

$is_positive(a)
```

The structure is readable without knowing the internals. A proposition is defined in terms of an existential over positive reals, a claim introduces a universally quantified variable with an implication, and a witness line supplies the existential that discharges it. The project points at a checked Cantor example in its Blueprint for a longer case, where a diagonal subset is defined, a general theorem is proved without a trust keyword, and the result is applied to a singleton function. That last point is the one to hold onto. The absence of a trust mechanism is the substantive claim of the project, and it is the reason the language exists rather than a general purpose proof assistant with a simpler syntax. The readme attributes the concision of the source to coordination among objects, facts, statements and verification procedures developed through sustained iteration, and says the Blueprint follows a small reciprocal function through that design from a systems engineering perspective.

## JSON feedback and a live session are what make AI collaboration workable

The design target for the tool is not a lone mathematician at a terminal. The readme says Litex is well suited to interactive work with AI, and describes a loop: the AI proposes a mathematical step, Litex checks it and returns feedback, and the AI revises or continues from accepted knowledge in the same session. The pipeline diagram on the project site shows checking a fact, finding local grounds, and making accepted knowledge available to later steps, and a second image previews the agent pipeline where the verifier returns JSON feedback and accepted facts accumulate into checked source. The tool's command line is what carries this. The CLI can present JSON verification feedback in several languages, so the same source can be checked with -lang zh for Chinese explanations or -lang fr for French ones, and the language setting changes the feedback rather than the statement being checked. The readme credits AI-assisted translation for making the multilingual explanatory copy feasible, which is a small and rather elegant piece of dogfooding. For machine consumers, the tool emits JSON with statement text, stored facts, inferred facts and proof summaries, and the readme warns that normal JSON summarises verification and does not expose every dependency, pointing at a documented JSON output contract. There is also a LaTeX export in preview, which compiles parsed source into mathematical LaTeX with prose in any of the ten CLI languages, and it preserves definitions and explicit proof steps without executing or verifying them.

## The session is a process, and rerunning a file throws work away

There is a piece of operational advice in the readme that is more important than it first appears, and it is stated as a warning. When writing or repairing Litex code, open -session and keep that process alive, because an ordinary failed statement preserves earlier accepted definitions and facts, and you should never rerun the whole file from the beginning whenever you add a few new lines. In other words, the accepted state of a proof lives in a running process, not only in the file on disk. That design has a clear motivation, since the AI collaboration loop depends on the verifier holding the accumulated context while a candidate statement is being repaired, and it also has a clear cost. If the session process dies, the accepted context is gone, and recovery means replaying the file, which the readme treats as the thing to avoid. The repository layout shows how much sits around this core. There is a src/ directory, a std/ directory for the standard library, a tests/ directory with named integration test targets in the manifest, an examples/ tree that includes an agent_session_demo directory alongside a knowledge_base directory, a lean/ directory, a demos directory, dist/ for packaging, a Dockerfile, and a wix/ directory. The examples also include negative and wd_negative directories, which suggests the test corpus deliberately covers statements that must be rejected, not only ones that must pass.

## Building, packaging and where the boundaries are

The Rust implementation is packaged under the name litex-lang with a library crate also called litex and a binary called litex whose entry point is src/main.rs. The manifest declares an Apache-2.0 licence, an edition of 2021, and keywords covering proof, formal-verification, theorem-prover and mathematics. It lists no dependencies at all, and the profile sections turn off debug info and incremental compilation for dev, test and release, with symbol stripping in release, which is consistent with a self-contained binary that has to start quickly. The Dockerfile is equally spare. It starts from debian:bookworm-slim, copies an architecture-specific binary to /usr/local/bin/litex, copies the standard library to /usr/share/litex/std, and points the environment at it:

```dockerfile
FROM debian:bookworm-slim
ARG TARGETARCH
COPY --chmod=755 litex-${TARGETARCH} /usr/local/bin/litex
COPY std /usr/share/litex/std
ENV LITEX_STD_PATH=/usr/share/litex/std
ENTRYPOINT ["litex"]
```

The LITEX_STD_PATH environment variable is the one configuration detail an installer has to get right, and it is visible in the container recipe rather than buried in documentation. The release cadence is unusual. The three most recent releases are all beta builds, 1.0.10-beta, 1.1.0-beta and 1.1.1-beta, and all three landed on 2026-10-14 and 2026-10-15, with the last push matching the newest tag. A project shipping three betas in two days is iterating fast, which suits an early-stage formal language but means the version you read about may not be the version you get. The project also keeps a Privacy_Policy.md, an AGENTS.md, and both English and Chinese documentation, with the official site at litexlang.com.

## Conclusion

golitex is worth trying if you want to write mathematics that a machine checks, in a language whose statements look close to set theory with Python-like syntax, and if you are willing to treat the checker's feedback as the source of truth rather than the documentation. It is the wrong tool if you need a mature proof ecosystem, a library of already formalised mathematics, or the ability to state arbitrary quantified theorems without building the supporting facts first, since the readme is explicit that the examples are not a claim that the verifier can invent an entire proof. Verify first that the standard library path LITEX_STD_PATH resolves in your installation, that your JSON consumer matches the documented output contract, and that the release you install is the beta line you tested against. The last push was on 2026-10-15 and the current release is 1.1.1-beta from the same day.

## FAQ

### What is Litex and what does golitex implement?

Litex is a formal language for writing checkable mathematics, and golitex is its Rust implementation, published as the litex-lang crate with a litex binary. It is created and maintained by Jiachen Shen.

### How does Litex check a statement?

You write the fact, and the checker searches for supported local grounds and reports the method it found, or where checking stopped. The readme is explicit that the verifier does not invent an entire proof from the final statement.

### Why should I keep a Litex session running instead of rerunning the file?

An ordinary failed statement preserves earlier accepted definitions and facts, so the readme says to open -session and keep the process alive rather than rerunning the whole file from the beginning after each edit.

### Can Litex output be used by other tools?

Yes. The CLI emits JSON with statement text, stored facts, inferred facts and proof summaries, and there is a preview LaTeX export that compiles parsed source into mathematical LaTeX in any of the ten CLI languages without executing or verifying the proofs.

### What licence is golitex released under?

Apache-2.0, as declared in the Cargo.toml manifest and the LICENSE file at the repository root. The project also ships a Privacy_Policy.md and a separate Chinese README.

## Sources

- [License: Apache-2.0](https://github.com/litexlang/golitex/blob/main/LICENSE)
- [litexlang/golitex on GitHub](https://github.com/litexlang/golitex)
- [Project website](https://litexlang.com)
- [README](https://github.com/litexlang/golitex/blob/main/README.md)
- [Releases](https://github.com/litexlang/golitex/releases)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/litexlang-golitex