Browse papers, proofs, Lean, and code
Searchable website · Reading routes · Hand-worked examples · Glossary · Reading downloads
Browse by mathematics, computer science, physics, or other and combine those filters with completion stage, Lean coverage, evidence basis, publication type, and a text query. The full-text search applies the same work-level classifications to indexed reading pages, claims, code, and guides. Or go directly to written statements and proofs, Lean sources, or code and scripts.
Each work has its own page with Read, Written proofs, Lean, Code, and Evidence sections. PDF opens a reading file. Text opens editable TeX or other source text. Lean guide opens explanatory reading. Lean sources leads to .lean files. Code links can include research utilities and build scripts. Read the edition's README before running them.
Browse by discipline and verification
| Primary field | Filtered catalogue |
|---|---|
| Mathematics | Mathematics works |
| Computer Science | Computer Science works |
| Physics | Physics works |
| Other | Methodology and cross-disciplinary works |
These are editorial primary categories. The files remain in their original repository paths so source links and formal evidence references are preserved. A finished reading edition is not necessarily a fully proved research endpoint. Completion, Lean coverage and evidence basis are independent, with details in the completion guide and status catalogue. Filter values come from the maintained project status manifest, not inferred from a file name or its presence in a folder.
Choose a publication type
| Collection | Open |
|---|---|
| Core papers | 12 works |
| Books and companion volumes | 19 works |
| Research programs | 49 works |
| Software packages | 5 works |
| Experiments | 5 works |
Follow a claim
- Open the work's PDF or text and find the theorem, proposition, or section number.
- Read the written argument and its assumptions. The proof finder links manuscript text, selected claim maps, and the existing evidence record.
- Where formalization exists, follow the Lean source finder and the edition's claim maps and build instructions. A similarly named declaration or a Lean-guide PDF does not by itself establish a correspondence.
- Use the work's Evidence section to see what was checked and what remains open. Written proofs do not require Lean.
Move around without opening large folders
Category pages have linked contents and direct file shortcuts. Choose Work page to keep one work's paper, proofs, Lean, code, and evidence together. Each work page has a section menu, return links, and previous/next links within its collection. Proof, Lean, and code sections link to their matching finder entry. Each finder links back to the same work section. The status catalogue links back to the same work page. Older category anchors remain usable.
Use your browser's Find command (Ctrl+F or Command+F) to locate a title. Links carry file-format labels, and status is written in text rather than conveyed by color. Work pages use a single-column list layout. TeX links provide source text where available. Some PDFs may lack the tags needed by assistive technology.
The original files remain in their source directories. If a PDF is too large for GitHub's preview, use the file page's download control. If a file is not linked here, check the edition's full file listing. The complete component index includes all supporting and historical collections.
Small examples and other editions
- Research Preview 1: mathematical note, claim map, and reproduction instructions.
- Corrected SRIC 0.3.3 runtime and its recorded checks.
- Independent libraries and earlier software editions.
- Incubator and return criteria. Incubator entries are marked separately on category pages and excluded from the proof, Lean, and code reading routes.
These are navigation links to preserved editions. See each work's evidence for the reviews and Lean runs completed so far.