Milestones

List view

• Proof Reconstruction Milestone 2: Remaining basic types

  Extend Proof Reconstruction implementation to the rest of the basic types. Deliverables: Lean-blaster repository updated including rules for: - String - Quantifiers (ForAll and Exists) - ITE and dite normalization - Projection Acceptance Criteria: - Proof reconstruction implemented for all remaining basic types. - Lean-blaster updated with String, Quantifiers (ForAll/Exists), ITE/dite normalization, Projection, and remaining agreed rules, with all tests passing.

  Due by November 12, 2026

  •0/15 issues closed
  0% complete15 open0 closed

• Update to latest Lean 4 > 4.33

  Let's move to a newer version

  Overdue by 29 day(s)

  •

  Due by September 30, 2026

  •0/3 issues closed
  0% complete3 open0 closed

• Proof Reconstruction Milestone 1: Core basic types

  Extend proof reconstruction to the arithmetic and logic types that follow the same pattern already used for Nat. Deliverables: - Int arithmetic and relational rules - Bool binary operations - Prop connectives (and, or, and the binary rules) - Decide and DecideBoolBinary rules - Hardening of the existing Eq coverage Acceptance criteria: The optimization tests for Int, Bool, Prop, and Decide pass with reconstructed proofs and never fall back to admit.

  Overdue by 1 month(s)

  •

  Due by September 28, 2026

  •9/21 issues closed
  42% complete12 open9 closed