TODO: What's Next for Litex

A roadmap for the Litex-to-Lean compiler, Python and C generation, and a growing collection of mathematical textbooks. These are development plans; each track starts from existing work and sets out the next artifacts to build and check.

The goal is to make a readable mathematical development useful beyond a single successful check. Its definitions, domains, hypotheses, and proofs should remain available when the development becomes a Lean proof, an executable fragment, or a chapter that other people and AI agents can reuse.

The three tracks

This is an evolving TODO list. The milestones below describe intended work, not release dates or claims that whole-language compilation and complete textbook coverage already exist.

One mathematical development, several uses

Consider the problem from the beginner course: define the reciprocal of a nonzero real number and prove that its product with the input is one. The nonzero condition must survive every later use.

The planned connections are:

Mathematical problem
    -> .lit definitions, legal inputs, statements, and checked proofs
        -> Lean proof, then a separate Lean kernel check
        -> supported computation, then Python or C and execution checks
        -> textbook chapter with named concepts and reusable results

These destinations need different evidence. A Lean consumer needs a proof and its dependencies. A program needs an executable definition and a contract for its inputs and numerical behavior. A textbook reader needs the meaning of the definition, the mathematical proof idea, and the chapter's assumptions.

The reciprocal is a useful acceptance example for this roadmap: it tests whether the same nonzero domain is preserved through those different uses. It is a proposed common example, not a claim that every route currently accepts the complete course file.

1. Litex-to-Lean compiler

Goal

Write mathematics in Litex, then compile supported checked reasoning into Lean proofs that can be checked and used in the Lean/Mathlib ecosystem. The compiler should preserve the definition, assumptions, and actual proof dependencies of the source development.

GitHub: Lean compiler project and semantic interfaces, source/generated examples. For the current authoring and compilation contract, read the compiler guide and CLI boundary.

Starting point

Litex has a preview route for compiling supported checked source into Lean. Its supported surface is a subset of Litex; the proof route and construction evidence matter, not only whether the final mathematical sentence is true. The linked project contains semantic interfaces and paired examples. Public examples and implementation details evolve, so use the current compiler guide when choosing an example to regenerate.

A source check, successful code generation, and a successful Lean kernel check are three separate results. A semantic interface or explicit assumption in a generated theorem must also be understood before calling it a theorem about ordinary Lean/Mathlib mathematics.

TODO

• Grow support from real proof examples. Extend supported arithmetic, membership, functions, predicates, and proof constructions one checked source/generated pair at a time. Keep a nearby example that must still be rejected when its evidence or domain condition is missing.
• Preserve proof dependencies. Carry the facts used, input conditions, scopes, and construction checks into the emitted proof. Unsupported routes should identify the exact missing support rather than leave a proof hole.
• Complete the required semantic bridges. State precisely which Litex objects and rules have a proved interpretation in the target model, and make remaining foundation or interpretation work visible.
• Produce useful native statements. Where a handwritten adapter is needed, keep it separate from generated code. The final theorem should use ordinary Lean/Mathlib concepts, with the representation bridge proved in the adapter.
• Make regeneration reproducible. Preserve the Litex source, generated file, required interfaces, pinned toolchain, and the command that checks the result. Regeneration should detect drift in maintained example pairs.
• Scale to a mathematical module. Move from individual examples to a connected collection of definitions and theorems, with explicit coverage for dependencies and unsupported statements.

What a completed milestone should contain

For the reciprocal example, the final native theorem should express the ordinary real-number product law under the same nonzero hypothesis. A milestone needs the source proof, generated Lean proof, any required adapter, and an actual successful Lean check. Emitting plausible Lean text alone does not complete it.

The first broader target is a small module whose exported mathematical results can be used by a Lean project without the consumer having to reconstruct the original Litex proof by hand.

2. Litex-to-Python and C

Goal

Turn supported mathematical computations into usable programs while retaining the connection between the mathematical specification, legal inputs, and the generated implementation. Python serves interactive use and experiments; C serves compiled numerical code and integration with other programs.

GitHub: extraction pipeline and supported subset, Python backend, C backend.

Starting point

The experimental extractor supports numeric constants and a restricted real-valued algorithm surface. It shares a target-independent program representation before rendering Python or C. It is not a compiler for every Litex definition: a general have fn can be checked without producing an executable function.

Current Python output uses floating-point expressions; C output uses double and can be a translation-unit fragment rather than a complete application. A proof about exact source mathematics does not establish rounding accuracy, overflow behavior, or a target compiler's execution semantics.

TODO

• Publish complete executable examples. Pair a mathematical source with generated Python and C, legal sample inputs, expected outputs, and a small driver that actually runs the artifact.
• Expand the executable subset deliberately. Add the function, algorithm, and control-flow forms needed by useful examples. Keep a clear distinction between a mathematical existence proof and an implementable procedure.
• Preserve input contracts. Specify how generated programs handle inputs outside the source domain. For the reciprocal, accepting zero must not silently change the mathematical specification.
• Separate exact mathematics from numerical behavior. Document the target number representation. For numerical algorithms, state the error assumptions and test the claimed precision or convergence behavior.
• Keep the two backends consistent. Use the shared program representation and run the same accepted-input examples through both targets, with comparisons suited to their numerical contracts.
• Grow practical use cases. Develop small numerical routines, mathematical simulations, and algorithm examples with a readable proof or specification beside the generated program.

What a completed milestone should contain

A small bundle should contain the mathematical specification, the checked Litex source, generated .py and .c files, a C build/run entry point, and checks for both legal inputs and the nearest rejected input boundary. Its documentation should say which property was checked mathematically and which behavior was checked by running the target program.

For the reciprocal, this includes a visible policy for zero and a description of the floating-point result. Later numerical examples can add bounded-error or convergence claims when those claims have their own evidence.

3. Textbooks and reusable mathematics

Goal

Develop mathematical textbooks as connected Litex projects. A chapter should teach its concepts and proof ideas while leaving definitions and theorems that later chapters and AI agents can read, check, and reuse.

GitHub: public textbook collections. The website textbook reader provides another way to explore the published material.

Starting point and directions

Existing public collections provide four natural directions for continued work. Their presence is not a claim that every chapter or exercise is fully verified; consult each collection's documentation for its coverage and proof boundaries.

TODO

• Keep a mathematical reading path. Introduce definitions when the mathematical story needs them, explain the proof idea, and then show the checked Litex construction. Preserve the difference between understanding a concept and merely finding syntax that passes.
• Record coverage by source item. Identify which definitions, propositions, and exercises are represented, checked, or still blocked. Include attribution and the source location without reproducing material that cannot be redistributed.
• Build reusable concept interfaces. Keep domains and nondegeneracy conditions in the definitions, and let later chapters consume established functions and theorem interfaces instead of rebuilding them.
• Track and reduce proof debt. Make explicit assumptions and unproved steps visible. Keep concrete blocker examples so missing library, language, or verifier support can be investigated.
• Check chapters in their real project context. Maintain ordered dependencies and verify a changed chapter with its actual preceding context. A whole-book claim needs a separate whole-book check.
• Connect the compiler work to selected chapters. Choose small slices that can yield Lean proofs or executable examples. Publish the accepted slice and its boundaries before expanding to a whole book.

What a completed milestone should contain

A maintained chapter should have a coherent mathematical narrative, source attribution, a runnable module entry, a coverage record, reusable interfaces, and verification evidence with explicit assumption and proof-debt boundaries. Representative exercises should show how a reader uses those interfaces.

The next unit of progress is a connected, checked chapter slice. The longer term goal is a library of such developments that students and AI agents can build on without losing the original mathematical meaning.

How the tracks support each other

Textbook work supplies real definitions and proofs that expose compiler and library gaps. Lean compilation supplies a separate target proof check for the supported evidence. Python and C generation turn suitable constructions into computations whose execution can be inspected.

This serves the broader math for AI direction: provide mathematical interfaces and reusable checked knowledge that AI agents can work with. Whether the workflow reduces the cost of construction, review, or repair is a research question to measure through real examples.

Milestone record

For each completed example or chapter slice, the intended record is:

This page records intended development. As milestones acquire concrete artifacts and acceptance evidence, update their status and link those results from the relevant track.

Share your suggestions

If you have ideas for Litex, suggestions for this roadmap, or mathematical problems you would like to see supported, please get in touch. You can email me at litexlang@outlook.com or share your suggestion in a GitHub issue.