List of blueprints

Stream: maths

[Bas Spitters]

Is there a (partial) list of Blueprints somewhere?

[Rémy Degenne]

Those two github repositories list some of them in their readme: https://github.com/PatrickMassot/leanblueprint, https://github.com/pitmonticone/LeanProject

[Bolton Bailey]

It would be nice if these were indexed more thoroughly. Here's all the ones I found:

"https://github.com/AlexKontorovich/PrimeNumberTheoremAnd"
"https://github.com/Bergschaf/Localic-Caratheodory-Extensions"
"https://github.com/Bergschaf/lean-banach-tarski"
"https://github.com/BoltonBailey/FRISoundness"
"https://github.com/CBirkbeck/DirichletNonvanishing"
"https://github.com/CBirkbeck/WeilConverse"
"https://github.com/Command-Master/lean-bourgain"
"https://github.com/ElifUskuplu/Stlc_deBruijn"
"https://github.com/FredRaj3/SemicircleLaw"
"https://github.com/ImperialCollegeLondon/FLT"
"https://github.com/Ivan-Sergeyev/seymour"
"https://github.com/LeastAuthority/STIR"
"https://github.com/RemyDegenne/CLT"
"https://github.com/RemyDegenne/brownian-motion"
"https://github.com/RemyDegenne/testing-lower-bounds"
"https://github.com/RikHeurter/LeanBscThesisFormalisation"
"https://github.com/Shreyas4991/DGAlgorithms"
"https://github.com/Verified-zkEVM/ArkLib"
"https://github.com/WuProver/groebner_proj"
"https://github.com/Xiyou-Wu/RiemannianGeometry"
"https://github.com/YaelDillies/ChandraFurstLipton"
"https://github.com/YaelDillies/LeanAPAP"
"https://github.com/YaelDillies/LeanCamCombi"
"https://github.com/YaelDillies/Toric"
"https://github.com/acmepjz/lean-iwasawa"
"https://github.com/ahhwuhu/zeta_3_irrational"
"https://github.com/andrejbauer/partial-combinatory-algebras"
"https://github.com/b-mehta/ABC-Exceptions"
"https://github.com/emilyriehl/infinity-cosmos"
"https://github.com/fpvandoorn/BonnAnalysis"
"https://github.com/fpvandoorn/carleson"
"https://github.com/ivankobe/FactorizationSystems"
"https://github.com/kkaunda/spgf"
"https://github.com/kkytola/ExtremeValueProject"
"https://github.com/leanprover-community/con-nf"
"https://github.com/leanprover-community/flt-regular"
"https://github.com/leanprover-community/sphere-eversion"
"https://github.com/loganrjmurphy/LeanEuclid"
"https://github.com/mkaratarakis/HopfieldNet"
"https://github.com/mo271/FormalBook"
"https://github.com/morganfshirley/CommComp"
"https://github.com/oliver-butterley/SpectralThm"
"https://github.com/pitmonticone/NewProject"
"https://github.com/provables/sequencelib"
"https://github.com/quangvdao/ZKLib-deprecated"
"https://github.com/shetzl/autth"
"https://github.com/teorth/equational_theories"
"https://github.com/teorth/expdb"
"https://github.com/teorth/pfr"
"https://github.com/utensil/LeanBlueprintExample"
"https://github.com/vbeffara/RMT4"

[Michał Mrugała]

Also

https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean

[Kevin Buzzard]

(the latter project was only made public today!)

[Bhavik Mehta]

https://github.com/b-mehta/unit-fractions also has a blueprint

[Bolton Bailey]

I scraped reservoir to get a list of lean repos - seems these projects aren't (yet) indexed by reservoir.

[Bhavik Mehta]

The sphere packing project was perhaps too new to be on reservoir, and unit-fractions is too old to be on reservoir :)