❓ How to use this library
Blueprints — all the papers and their blueprints. Each piece below can be shown on the page: «Show me».
The library of blueprints
All the papers, each with its blueprint: every statement, how they depend on each other, and what was checked besides the proofs. This short tour shows the pieces of this page.
Search every paper at once
Type a statement number, a name or a word (3.4, atom, Lean, program…): the matching statements of all the papers appear below. Press / to come back here.
Show meChoose a subject
A keyword, an MSC code, a field or a tool: only the papers and statements that carry it stay.
Show meWhat was checked
Show only the results formalized in Lean, the ones checked by a program, the ones with a written proof only, or the main results.
Show meThe library in numbers
How many papers and results, and how many of them were checked by Lean or by a program.
Show meIts results, one tile each
Each tile is a numbered result of the paper; its colour says what checked it. A tile opens its statement.
Show meOpen it
📘 the blueprint, 🗺️ the map of its results, 📕 the paper as a PDF, 🔗 the published record.
Show meThe list of papers
Click a paper: it opens here, with its own bar on top (Blueprint, Map, PDF, Graph); 🏛️ Atlas brings you back.
Show meOther ways to arrange them
By series, by MSC code, by the branches they take tools from, by what they serve, or as the Lean formalizations, module by module.
Show meHow to read the colours
Green: formalized in Lean (dashed: a part). Blue: checked by a program. White: written proof only.
Show meThat is all
🧭 Tour repeats this tour; ❓ How to use explains each piece. Each paper's blueprint has its own tour.
Your browser can translate these pages (the formulas stay as they are).