[NeurIPS 2025 Spotlight] TPA: Tensor ProducT ATTenTion Transformer (T6) (https://arxiv.org/abs/2501.06425)

NanoGPT (124M) in 90 seconds

A minimal development of SSA theory

Definitional implementation of Cedar language and utilities for DRT

The best ChatGPT that $100 can buy.

Original Apollo 11 Guidance Computer (AGC) source code for the command and lunar modules.

HPC Rust LLM Tokenizer Suite

A Proof-oriented Programming Language

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