Issues

• Seven examples carry the literal example's \title{Natural number addition}

  UOR-Foundation/LexLean#251 · Filter by author afflom opened on Oct 21, 2026 · LexLean v0.4

• v0.5: proof-language step for fuel arithmetic under symbolic depth (nested-key equation theorems of SP-25)

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

• The elan step of the gate has no retry; a transient HTTP 500 from releases.lean-lang.org fails a leg before any test runs

  ci
  UOR-Foundation/LexLean#242 · Filter by author afflom opened on Oct 20, 2026 · LexLean v0.5
  1

• [0.5.0] surface::module::locate classifies a module by the first marker in kind order, not by the envelope the parser opens

  UOR-Foundation/LexLean#241 · Filter by author afflom opened on Oct 20, 2026 · LexLean v0.5

• The Intel macOS host leg has crept from ~60 to 100+ minutes; bring its cost down

  ci
  UOR-Foundation/LexLean#235 · Filter by author afflom opened on Oct 20, 2026

• Certificate generator: a derived _unsafe_rec row depends on propext once six expr:call elements join the table of correspondCrate (LLV7013)

  UOR-Foundation/LexLean#222 · Filter by author afflom opened on Oct 20, 2026
  1

• [v0.5] SP-17 writes down what it cannot see and matches its allow-list exactly (follow-up to #167)

  bug
  UOR-Foundation/LexLean#181 · Filter by author humuhumu33 opened on Oct 18, 2026 · LexLean v0.5
  1

• [v0.5] Plant evidence states what it shows: generator refusals by locus, SP-16's forged-program plant, the SM-32 records (follow-up to #167)

  bug
  UOR-Foundation/LexLean#179 · Filter by author humuhumu33 opened on Oct 18, 2026 · LexLean v0.5
  1

• production: a generated rust-std package can need more rustc stack than a default Windows thread gives (found by #160)

  UOR-Foundation/LexLean#164 · Filter by author afflom opened on Oct 17, 2026
  2

• [0.5.0] Release 0.5.0

  UOR-Foundation/LexLean#128 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5
  1

• [0.5.0] κ-addressing in LexLean, validated against uor-addr

  UOR-Foundation/LexLean#127 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] Self-application: the compiler carries its own optimality certificate

  UOR-Foundation/LexLean#125 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] A general performance corpus

  UOR-Foundation/LexLean#124 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] Bridge from certified cost to measured wall time

  UOR-Foundation/LexLean#123 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] Universal lower-bound library generated from the Atlas (universal data handles)

  UOR-Foundation/LexLean#122 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] The realization universe of a production root, defined by grammar before optimization

  UOR-Foundation/LexLean#120 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] Production export requires a global_optimal certificate

  UOR-Foundation/LexLean#121 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] Machine contracts for production targets with exact instruction semantics

  UOR-Foundation/LexLean#119 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] Discharge the overflow effect with a kernel-checked bound

  UOR-Foundation/LexLean#116 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] Content-addressed artifacts as compile-time constants of production roots

  UOR-Foundation/LexLean#115 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5
  5

• [0.5.0] Release identity: §2.3 and §30 for a 0.5.0 release covering languages 1.0–1.2

  UOR-Foundation/LexLean#113 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [0.5.0] State the production path and the optimality guarantee in LexLean's purpose and scope

  UOR-Foundation/LexLean#112 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5

• [decision] D7: location of κ-addressing written in LexLean

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

• [0.5.0] Normative text as LexLean source: SPEC.md and model/*.toml as generated projections

  UOR-Foundation/LexLean#111 · Filter by author afflom opened on Oct 15, 2026 · LexLean v0.5
  7

• [decision] D4: target machines and feature sets modeled first

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