The bibliographic spine of this corpus — titles, authors, journals, DOIs, MSC classification and the citation graph — comes from zbMATH Open.
License: CC-BY-SA 4.0. Rights holder: FIZ Karlsruhe GmbH — zbMATH Open. Data has been modified by normalization; see the license text. Reviews, reviewer identities, abstracts and keywords are deliberately absent: not redistributable under these terms, and reviewer names are personal data. This index is bibliographic only.
zbMATH does not license every field it holds. On some records it withholds the title — usually the author list with it — so those entries would otherwise show nothing but a journal name and a DOI. Crossref and OpenAlex supply the missing values, from metadata deposited by the publishers themselves. Nothing else is taken, and a field zbMATH does supply is never overwritten.
Basis: titles and author lists are facts about a publication rather than editorial content. Crossref places no copyright claim on its metadata.
Attribution follows the field, not the record. Every recovered value is stored with its own source and licence, and each affected paper records which of its fields did not come from zbMATH.
Crossref does not hold every DOI — its coverage thins for older expository and statistics journals. OpenAlex, which aggregates Crossref and adds repository and publisher records, fills part of what remains. Between the two, 177,173 papers carry a recovered title and 170,496 a recovered author list; entries with no usable title stand at 26,287, about 0.5% of the corpus.
Licensed: CC0 1.0 — a public-domain dedication, the most permissive terms of any source used here. Only title and authors are taken, only where zbMATH withheld them and Crossref had nothing, and each value carries its own provenance.
5,078 of the remaining entries carry no DOI and no arXiv identifier, so there is nothing to look them up by. They appear under their journal and year.
Databases excluded, and why:
Google Scholar offers no API and prohibits automated queries. Semantic Scholar carries mixed licences including CC BY-NC, whose non-commercial restriction does not compose with the rest of this corpus. MathSciNet is a subscription service whose terms forbid redistribution.
A few entries reference The Stacks Project, a continuously-updated collaborative reference. Only bare bibliographic facts are recorded — title, collective authorship, URL — never its definitions, theorems or text.
Licensed: GNU Free Documentation License, The Stacks Project Authors. Only bibliographic facts are recorded.
A registry of Lean-verified mathematics, incubated by the Lean FRO and ICARM. Each entry pins an immutable commit and records the exact statement checked, its dependencies, toolchain, permitted axioms, and the result of the proof check by Lean’s kernel and an independent checker. A link to a Palomar entry is machine-verified evidence rather than an assertion.
What is taken: the repository URL and commit, the names of the checked declarations, and the verification status — facts about a public artifact. No mathematical content is copied. The correspondence between a checked statement and the published paper it formalizes is established by this index, and every such link is checked against the author list of the candidate record before it is recorded.
Terms: bare bibliographic facts only — repository, commit, declaration names — as with the Stacks Project entry above.
A collaborative platform for formalizing mathematics in Lean 4 (prove2.me), whose proved results are collected in Formalpedia. Papers formalized in a completed Prove2Me mission link to that mission.
Terms: Apache 2.0; only links and facts about missions are recorded here.
A public collection of mathematical manuscripts produced by an internal OpenAI model and published by OpenAI (github.com/openai/math), many with Lean formalizations of their main results. Each manuscript is recorded here as its own entry, with a MiND code, and its formalization linked to the exact Lean declarations. Where the release proves in Lean a theorem from an earlier published paper, that paper is linked too, stating, where known, whether the theorem was proved in full, as a special case, or reformulated.
Status: shown as unverified, with no formalization score: the proofs have been checked by OpenAI only, not independently. Terms: Apache 2.0; only bibliographic facts and links to the release are recorded here, pinned to a fixed version of the repository.
An open Lean library downstream of Mathlib (github.com/TauCetiProject/TauCeti), written by AI agents from roadmaps set by mathematicians. It develops its own treatment of the areas it covers.
Status: score 100 by construction. Terms: Apache 2.0; bibliographic facts and links only.
The community math library of Lean 4 (github.com/leanprover-community/mathlib4) and the foundation on which most other Lean formalization projects are built. Written and reviewed by its contributors and maintainers, it develops its own treatment of the areas it covers.
Status: score 100 by construction. Terms: Apache 2.0; bibliographic facts and links only.
Other openly-licensed mathematical archives with comparable terms could extend this corpus the same way. Not yet integrated, but under consideration:
The formalization scores, correctness profiles and original analysis in this database are the independent work of this project, distinct from the bibliographic facts above. Terms in full:
License: CC BY-SA 4.0, as required by the terms it was harvested under. Attribution: “Contains information from zbMATH Open, made available under CC-BY-SA 4.0 by FIZ Karlsruhe. Data has been modified by normalization.” That notice must survive any further extraction. Reviews, reviewer identities, abstracts and keywords are excluded and are not redistributed by this project in any form.
Original analysis produced by this project, published under the same CC BY-SA 4.0 terms as the corpus it annotates, so the database can be reused as one coherent work rather than as parts under conflicting conditions.
License: Apache License 2.0. The code that harvests, normalizes, scores and serves this index is licensed separately from the data it processes — a permissive code license does not place the CC-BY-SA corpus under those terms, and the corpus’s share-alike obligation does not reach the code.