Issues

• Bumping mathlib to 728a93e would break the build

  dependency-incompatibility
  leanprover/cslib#1017 · Filter by author github-actions opened on Oct 1, 2026

• delete once [Mathlib PR 44381](https://github.com/leanprover-community/mathlib4/pull/44381) is available. -/

  leanprover/cslib#1013 · Filter by author github-actions opened on Oct 1, 2026

• delete once [Mathlib PR 44381](https://github.com/leanprover-community/mathlib4/pull/44381) is available.

  leanprover/cslib#1012 · Filter by author github-actions opened on Oct 1, 2026

• Rename Parallel => ParBeta or FullBeta.Parallel

  leanprover/cslib#990 · Filter by author lengyijun opened on Sep 29, 2026

• upstream this generalisation of Mathlib's smulCommClass_self, which applies only to

  leanprover/cslib#824 · Filter by author github-actions opened on Aug 20, 2026

• upstream this generalisation of Mathlib's smulCommClass_self, which applies only to

  leanprover/cslib#823 · Filter by author github-actions opened on Aug 20, 2026

• adapt topNamespace to the module system

  leanprover/cslib#790 · Filter by author github-actions opened on Aug 10, 2026

• listFullBeta_cons_r should rename to listFullBeta_concat_r

  leanprover/cslib#784 · Filter by author lengyijun opened on Aug 9, 2026

• Add tests for capture-avoiding substitution in lamba calculi

  help wanted
  leanprover/cslib#711 · Filter by author chenson2018 opened on Jul 12, 2026
  2

• feat(Computability): quantum computing foundations

  leanprover/cslib#688 · Filter by author exAClior opened on Jul 1, 2026

• Proposal: lawful lenses for verified state access

  leanprover/cslib#658 · Filter by author fraware opened on Jun 17, 2026

• IsIntuitionistic should be generalised outside the PL scope, once we have typeclasses to express that a type possesses an implication connective.

  leanprover/cslib#655 · Filter by author github-actions opened on Jun 16, 2026

• this should be

  leanprover/cslib#654 · Filter by author github-actions opened on Jun 16, 2026

• this should

  leanprover/cslib#653 · Filter by author github-actions opened on Jun 16, 2026

• this should

  leanprover/cslib#652 · Filter by author github-actions opened on Jun 16, 2026

• Logics and WP calculi: First-order logic, Second-order logic, Henkin semantics, Separation Logic

  leanprover/cslib#646 · Filter by author praalhans opened on Jun 14, 2026

• develop an attribute to dualize theorems to the converse of a relation

  leanprover/cslib#644 · Filter by author github-actions opened on Jun 13, 2026

• TimeM's ✓ tick breaks when HasWellFormed is imported

  leanprover/cslib#638 · Filter by author FrankieNC opened on Jun 12, 2026

• feat(Computability): Plan for complexity theory

  leanprover/cslib#611 · Filter by author crei opened on Jun 1, 2026
  2

• Loogle for Cslib

  leanprover/cslib#594 · Filter by author SamuelSchlesinger opened on May 23, 2026
  1

• feat(Computability): Framework for encoding arbitrary types on Turing machines

  leanprover/cslib#590 · Filter by author Sfgangloff opened on May 21, 2026

• feat: Mergesort Stability

  leanprover/cslib#438 · Filter by author Arleee1 opened on Mar 18, 2026
  1

• feat(CellularAutomata): One-Dimensional Cellular Automata for Language Recognition

  leanprover/cslib#407 · Filter by author hediet opened on Mar 8, 2026
  1

• timing of bump_toolchain_nightly-testing.yml

  leanprover/cslib#394 · Filter by author chenson2018 opened on Mar 3, 2026

• Define the weak exponential of two LTSs

  leanprover/cslib#390 · Filter by author ayberkt opened on Mar 2, 2026