Issues

• [v0.4] Refuse the data form (\semanticdata, \toolingdata, \coredata) under language 1.2: the last change of the milestone

  enhancement
  UOR-Foundation/LexLean#149 · Filter by author afflom opened on Oct 16, 2026 · LexLean v0.4

• Proposal: the PR gate verifies UOR Atlas by main's signed attestation, not by re-proving it (§9.4)

  UOR-Foundation/LexLean#131 · Filter by author humuhumu33 opened on Oct 15, 2026
  2

  

• [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] Release 0.5.0

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

• [0.5.0] SHA-256 in LexLean for every content identity

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

• [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] IEEE-754 bit patterns as exact dyadic rationals

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

• [0.5.0] Lemmas for universal equalities over list folds

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

• [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

• [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] Byte-to-fixed-width conversion in the language-1.2 surface

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

• [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

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

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

• [decision] D2: realization grammar and claim class for every production root

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

• [decision] D3: formulation of universal data handles generated from the Atlas

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

• [0.5.0] Completion plan: optimal compilation for every production root

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