Lemmata Repository

A living archive of mathematics. Every entry is written twice: once for people, in the prose you are reading, and once for Lean, in a formal proof that the kernel has checked.

Lemmata is a home for formalized results that are worth sharing before, or without, a full paper: lemmas and constructions that may never become a paper of their own but are still useful to others, and results at a stage before a preprint — a way to disseminate them early, with the Lean proof as evidence. It is equally a place to archive the formalization of results from a paper, preprint or published, linked to it, so the proofs have a permanent, citable home next to the text. Entries are self-contained, and each has a stable identifier to cite.

Entries are web pages rather than papers. They are written in MyST Markdown and rendered as HTML with KaTeX, so an entry can use what fits the mathematics — numbered results, diagrams, interactive widgets — instead of a fixed paper layout. We chose HTML on purpose: almost any information can be represented in it well, more richly than in a static document Shihipar, 2026.

The repository is also built to be read by machines, and by language models in particular. /llms.txt is a plain-text overview of every entry with its identifier and status; /lemmata.json is a machine-readable index with every exported Lean declaration, its verification status and axioms, and a BibTeX entry. Every entry links the Lean source of each result, and its page can be downloaded as Markdown. Coding agents that want to contribute follow AGENTS.md (linked below), the contribution procedure written for them.

Contributing. The archive is a Git repository, github.com/ZIB-IOL/lemmata. New entries and changes arrive by pull request; the contribution guide (and AGENTS.md, the same procedure written for coding agents) explains every step. The site rebuilds itself from main within minutes; the build status shows which version is live and, for a commit that was not published, why.

Entries¶

cs.CC — Computational Complexity¶

math.OC — Optimization and Control¶

cs.IT — Information Theory¶

math.CO — Combinatorics¶

math.LO — Logic¶

quant-ph — Quantum Physics¶

Topics¶

Extended formulations (5) · Nonnegative rank (1) · Common information (2) · Tensor rank (3) · Arithmetic circuits (1) · Reed–Muller codes (2) · Duality (1) · Frank–Wolfe and linear oracles (1) · Worked examples (1) · Bell inequalities (1)

What “checked” means here¶

A kernel-checked result is one whose formal statement compiles and was accepted by Lean’s kernel, using only the standard axioms. That the English statement means the same as the Lean statement is checked by human review. Read the full definition.

For what “verified in Lean” does and does not establish, and what a reader should still check, we recommend the essay by Spiegel (2026).