# Research Positioning
Jiachen Shen and The Litex Team, 2026-05-21. Email: litexlang@outlook.com
Markdown source: https://github.com/litexlang/golitex/blob/main/docs/Research_Positioning.md
## Thesis
Litex explores a fact-oriented interface for ordinary mathematical reasoning.
The user states mathematical facts, and the verifier grows an explainable
checked context by checking well-definedness, builtin rules, known facts, and
known universal facts.
Litex is intentionally narrower than Lean, Coq, or Isabelle. It does not
compete on library depth, foundational generality, or production maturity. Its
research question is different:
> Can a proof language reduce proof-engine bookkeeping for textbook-style
> mathematics by making facts, context growth, and verifier feedback the main
> interface?
## Design Point
Most Litex scripts are sequences of proof actions over mathematical facts:
introduce an object, state a fact, prove a local claim, name witnesses from an
existential, split cases, or record a reusable universal fact.
The checker tries to make common mathematical structure directly usable:
- equality chains;
- membership and subset reasoning;
- arithmetic and order facts;
- finite set and tuple facts;
- function-domain and function-value facts;
- existential witnesses;
- universal statements matched by shape.
This makes the proof script look closer to a textbook argument. The user often
states the next mathematical fact directly instead of choosing a tactic or
library lemma that packages the same move.
## Relation to Mature Proof Assistants
Lean, Coq, and Isabelle are mature systems with deep foundations, substantial
automation, large libraries, and expert communities. Litex should not be
presented as a replacement for them.
Litex explores another point in the design space:
- set-theoretic surface rather than a type-theoretic programming surface;
- facts and statements rather than proof terms as the main user interface;
- context growth rather than tactic-state navigation as the primary proof
metaphor;
- builtin ordinary mathematics rather than user-visible reconstruction of every
basic concept.
This design is less general. The possible benefit is lower interaction cost for
ordinary textbook mathematics and clearer local feedback for proof repair.
For a detailed comparison with Lean, see
[Litex vs Lean](https://litexlang.com/doc/Litex_vs_Lean).
## Research Questions
Litex is useful if it helps answer concrete questions:
1. Does fact-oriented proof writing reduce bookkeeping in textbook
formalization?
2. Which mathematical concepts should be primitive at the surface, and which
should be library-defined?
3. How large can builtin mathematical background become before it hurts
trust, debugging, or portability?
4. Can verifier output explain accepted facts well enough for users to audit
proof steps?
5. Does local fact-level feedback help AI agents repair proofs more effectively
than lower-level proof states?
6. Can Litex serve as a preformal or intermediate layer for systems with deeper
foundations and larger libraries?
## Best Current Demo
The strongest demo is The Mechanics of Litex Proof. It translates a sequence of
textbook-style proof examples into Litex and shows the intended interaction:
write mathematical facts, run the checker, inspect the local explanation, and
continue growing the context.
The Chapter 8 construction of a bijection from `N^2` to `N` is especially
important. It is large enough to exercise functions, tuples, arithmetic,
existential witnesses, injectivity, surjectivity, and reusable facts. It is
also still close to ordinary undergraduate mathematics.
## What to Evaluate
For proof assistant researchers, the most useful feedback is not whether Litex
is already mature. It is not.
The useful questions are:
- Is the soundness boundary stated clearly enough?
- Are the builtin rules a reasonable way to expose ordinary mathematical
background?
- Does the fact-oriented interface remove meaningful proof-engine bookkeeping?
- Which interface ideas could be useful in other theorem-proving or
autoformalization systems?
- Which parts of the current design are too ad hoc to scale?