Issues

• FOL: revisit Valid/ValidT, Implies/ImpliesL and empty domains

  contentneeds-decision
  cslib-community/CSwL#36 · Filter by author arademaker opened on Oct 14, 2026

• FOL: bundle the structure (D, I, F) into a Lean structure

  enhancementneeds-decision
  cslib-community/CSwL#35 · Filter by author arademaker opened on Oct 14, 2026

• Reader-facing labels generated by CSwLMeta are inconsistently localized

  infrastructureneeds-decisionstyle
  cslib-community/CSwL#28 · Filter by author arademaker opened on Sep 20, 2026

• Cross-references to exercises are not possible

  infrastructurelater
  cslib-community/CSwL#24 · Filter by author arademaker opened on Sep 14, 2026

• Deferred: reuse Mathlib and CSLib in two written chapters

  later
  cslib-community/CSwL#20 · Filter by author arademaker opened on Sep 11, 2026

• Adopt a proofreading pass with a rejection ledger

  infrastructurelater
  cslib-community/CSwL#19 · Filter by author arademaker opened on Sep 11, 2026

• Understand the autograder before committing to it

  infrastructureresearch
  cslib-community/CSwL#17 · Filter by author arademaker opened on Sep 11, 2026

• Revise English.lean

  contentcontent-organization
  cslib-community/CSwL#15 · Filter by author arademaker opened on Sep 11, 2026

• The inference engine's interactive loop is not ported

  contentneeds-decision
  cslib-community/CSwL#14 · Filter by author arademaker opened on Sep 11, 2026

• Lean features used without being presented

  style
  cslib-community/CSwL#7 · Filter by author arademaker opened on Sep 11, 2026

• Two paragraphs defend an editorial choice in the book's prose

  style
  cslib-community/CSwL#5 · Filter by author arademaker opened on Sep 11, 2026

• doc-gen4: lake build Book:docs tenta documentar todo o Mathlib

  cslib-community/CSwL#1 · Filter by author arademaker opened on Aug 15, 2026