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
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
```