Issues

• Migrate the Verify proofs off the legacy do elaborator

  digama0/lean4lean#31 · Filter by author kim-em opened on Aug 4, 2026

• Prove Level cached-flag correctness

  digama0/lean4lean#24 · Filter by author kim-em opened on Aug 2, 2026

• NormLevel.subsumption_eval is false for arbitrary NormLevel

  digama0/lean4lean#18 · Filter by author thomasahle opened on Jul 31, 2026

• v4.26.0 and v4.29.0: cannot replay Init.Prelude/Init.Core (SIGSEGV; unknown constant 'String.ofList')

  digama0/lean4lean#17 · Filter by author agent-maestro opened on Jul 30, 2026
  1

• Contributing proofs

  digama0/lean4lean#16 · Filter by author thomasahle opened on Jul 30, 2026