About: point at the other efforts to organize Lean code

[teorth]

Prompted by somebody asking why their own library was not mentioned by Palomar.

The framing names projects by Lean FRO affiliation, and says so in the same sentence that lists them ("Lean FRO-supported libraries include…", then "In addition there are multiple additional libraries or registries of Lean code not affiliated with the Lean FRO"). That matters for the question that prompted it: an absence then reads as unaffiliated rather than as a judgement on the project. Palomar is itself Lean FRO-incubated, so a list of Lean FRO projects published here needs its criterion visible rather than implied.

Reservoir and its inclusion criteria carry most of the practical value: it is the Lean FRO's automatic package index, the criteria are published, and it is somewhere concrete for a library seeking an index to go.

Checked

• Mathlib links the library at leanprover-community/mathlib4. An earlier draft linked mathlib-initiative.org, which is a different thing — the Mathlib Initiative is "a program of Renaissance Philanthropy" funded by Alex Gerko and XTX Markets, and is explicitly distinct from the library.
• Hex — leanprover/hex, "Verified computational algebra in Lean 4", under the leanprover organization.
• Reservoir — operated by the Lean FRO; indexes, builds and tests automatically, against published inclusion criteria rather than indexing everything.
• Tau Ceti — its README says it is "being incubated by the Lean FRO and the Mathlib Initiative", so it is Lean FRO-supported but not solely.

Two a reviewer should confirm

• CSLib's own site lists sponsors (Amazon, Google DeepMind, Stanford Center for Automated Reasoning) and states no Lean FRO relationship. It may well be supported by them, but I could not verify it publicly, and it is the one entry whose presence depends on the stated criterion being true.
• The Zulip channel number (579630, "Project announcements") — the Zulip web app does not render for a fetch and search did not surface it.

Placed before "What about other proof assistants?", the page's other "what else is out there" question.

Test suite is unchanged by this edit: 254/261 both with and without it on the same checkout.

🤖 Generated with Claude Code