How big will "CSLib" be at the end of 2026?
6
Ṁ484
2026
1%
No CSLib has been publicly released
3%
less than 1000 lines of Lean4 code
13%
1000 - 9999 lines of Lean4 code
23%
10000 - 99999 lines of Lean4 code
24%
100000 - 999999 lines of Lean4 code
13%
1000000 - 9999999 lines of Lean4 code
13%
10000000 - 99999999 lines of Lean4 code
11%
100000000 or more lines of Lean4 code

A recent announcement has been made on the Lean Zulip of a forthcoming "CSLib" library backed partially by the LeanFRO.

This question asks how many lines of code will exist in .lean files in this repository at the end of 2026. The repository hasn't been released as of market creation, but I will try to identify it when it is released.

"Lines of Code" here refers to "physical" lines of code, i.e. total number of lines in .lean files, regardless of whether those lines are comments or whitespace.

As an example, a sequence of commands might be:

git clone https://github.com/leanprover/cslib.git
cd cslib
wc -l **/*.lean

Get
Ṁ1,000
and
S1.00
Sort by:

Slides about the library here

bought Ṁ100 less than 1000 lines... NO

Due to a merging of two projects, the CSLib at the git URL listed above now exists! I expect this address to be the one I use to resolve this market. Currently the command result in an output of a total of 6374 lines of lean code.:
```

> wc -l **/*.lean

       6 Cslib.lean

     383 Cslib/Computability/CombinatoryLogic/Basic.lean

     242 Cslib/Computability/CombinatoryLogic/Confluence.lean

     145 Cslib/Computability/CombinatoryLogic/Defs.lean

     387 Cslib/Computability/CombinatoryLogic/Recursion.lean

     165 Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean

      59 Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean

      92 Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean

       3 Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/AesopRuleset.lean

     150 Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Basic.lean

     123 Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean

     247 Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean

     180 Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Properties.lean

     158 Cslib/Computability/LambdaCalculus/Named/Untyped/Basic.lean

     113 Cslib/ConcurrencyTheory/CCS/Basic.lean

     458 Cslib/ConcurrencyTheory/CCS/BehaviouralTheory.lean

      50 Cslib/ConcurrencyTheory/CCS/Semantics.lean

     195 Cslib/Data/FinFun.lean

     161 Cslib/Data/HasFresh.lean

      85 Cslib/Data/Relation.lean

     228 Cslib/Logic/LinearLogic/CLL/Basic.lean

     686 Cslib/Semantics/Lts/Basic.lean

    1263 Cslib/Semantics/Lts/Bisimulation.lean

     169 Cslib/Semantics/Lts/Simulation.lean

     134 Cslib/Semantics/Lts/TraceEq.lean

     136 Cslib/Semantics/ReductionSystem/Basic.lean

      12 Cslib/Syntax/HasAlphaEquiv.lean

      13 Cslib/Syntax/HasSubstitution.lean

      13 Cslib/Syntax/HasWellFormed.lean

      58 CslibTests/Bisimulation.lean

      21 CslibTests/CCS.lean

      21 CslibTests/HasFresh.lean

      20 CslibTests/LambdaCalculus.lean

     128 CslibTests/Lts.lean

      70 CslibTests/ReductionSystem.lean

    6374 total
```

Slides about the library here