This is a program that uses the Contributions tracker as a marquee display.

Gemma open-weight LLM library, from Google DeepMind

♞ lichess.org: the forever free, adless and open source chess server ♞

LEAN4 AUTO YOUTUBE LIVING

Train the smallest LM you can that fits in 16MB. Best model wins!

Lean 4 Zstandard (RFC 8878) decompression: C FFI bindings and pure-Lean implementation with formal proofs

Ground Zero: Lean 4 HoTT Library

This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

The mathematical study of type theories, in univalent foundations

A formalized proof of a version of the initiality conjecture

mimalloc is a compact general purpose allocator with excellent performance.

zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements

The Lean Computer Science Library (CSLib)

Mathlib search tool

The open source coding agent.

A verification toolchain for Rust programs

Nix binary cache implemented in rust (maintainer: @Mic92)

Manage a user environment using Nix [maintainer=@khaneliman, @rycee]

A monitor of resources

Plain-text declaration export for Lean 4

The Noisebridge Infrastucture

A fully standalone Spotify client for the terminal. Native streaming included, no daemon required.

‼️ No waybar here ‼️

Randomized Property-Based Testing Plugin for Coq