Issues

• [v0.4] Define production eligibility, root closure, and formal-only vs executable semantic boundary

  UOR-Foundation/LexLean#36 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Define typed Lean compiler-frontend/LCNF authority interface and verified named-root extraction

  UOR-Foundation/LexLean#35 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] End-to-end release closure, examples, documentation, packaging, and clean-checkout reproducibility

  UOR-Foundation/LexLean#34 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Extend vv for production compiler, GNAF certificates, Rust artifacts, and oracle falsification

  UOR-Foundation/LexLean#33 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Build model/reasoning stdlib composition and PrismPM application fixture

  UOR-Foundation/LexLean#32 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Add reasoning-machine semantics: state, rules, search, verification, iteration, and termination

  UOR-Foundation/LexLean#31 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Add language-model semantic components and compositional text-processing pipeline

  UOR-Foundation/LexLean#30 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Introduce closed Model, Realization, Contract, and Evidence semantics

  UOR-Foundation/LexLean#29 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Add PrismPM production export contract and stable compiler API

  UOR-Foundation/LexLean#28 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation

  UOR-Foundation/LexLean#27 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Integrate auser/lean4-prod strictly as a differential validation oracle

  UOR-Foundation/LexLean#26 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Prove source→target→Rust semantic preservation for production-eligible LexLean

  UOR-Foundation/LexLean#25 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Implement canonical Rust AST/rendering backend from the production calculus

  UOR-Foundation/LexLean#24 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Implement LexLean-native GNAF certification and global lower-bound attainment framework

  UOR-Foundation/LexLean#23 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Define independent complete-system candidate universe, machine contract, and objective order for GNAF

  UOR-Foundation/LexLean#22 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Define the production realization calculus and exact Rust target semantics

  UOR-Foundation/LexLean#21 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Add finite maps, sets, sequences, graph data, and deterministic state-threading primitives

  UOR-Foundation/LexLean#20 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Generalize total recursion, mutual recursion, well-founded recursion, and termination evidence

  UOR-Foundation/LexLean#19 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Add first-class functions, lambdas, higher-order composition, and closure-safe semantics

  UOR-Foundation/LexLean#18 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Generalize semantic types: recursive algebraic data, products/records, and parameterized inductives

  UOR-Foundation/LexLean#17 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Define language 1.2 and compatibility/migration contract

  UOR-Foundation/LexLean#16 · Filter by author afflom opened on Sep 29, 2026

• [v0.4] Release program: general formal programming, verified production compilation, and models/reasoning

  UOR-Foundation/LexLean#15 · Filter by author afflom opened on Sep 29, 2026