Recorded example
Plane Geometry
Coordinate geometry, reusable geometric vocabulary, and a midpoint proof. This recorded collection uses explicit axioms.
Explore Litex
Litex showcases
Mathematics, knowledge for AI, agent workflows, and applications beyond mathematics.
Mathematics
Read mathematical developments by textbook, or explore definitions and proofs by field.
Published
Number Theory
Divisibility, prime numbers, and proofs built from earlier facts.
Not published yet
Linear Algebra
Vector spaces, linear independence, and linear maps.
Not published yet
Analysis
Real numbers, sequences, and connected mathematical developments.
Math for AI
Give AI mathematical knowledge it can check, accumulate, and reuse.
Walkthrough
A language for checkable knowledge
AI proposes; Litex checks; accepted mathematical knowledge accumulates.
Guide
Mathematics with structured feedback
Inspect accepted statements, reasons for failure, and recorded knowledge in the CLI's JSON results.
Litex AI Agents
Propose a statement, inspect verification feedback, repair it, and keep the accepted context.
Walkthrough
The propose–check–repair loop
Follow a reciprocal example through an accepted definition, a rejected claim, and its repair.
Guide
Build an agent around a Litex Session
Keep context in one process, submit complete statements, and save accepted source for replay.
Beyond Mathematics
Explore checked rules and computations in games, programs, and other applications.
Interactive
Experimental
Litex Chess
A chess move reveals a broader pattern: check actions against the current scene and explicit rules, then commit only a checked state transition.
What is next?
Follow the plans for Lean, executable code, and more mathematical collections.
Read the roadmap