loading corpus stats…
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.
Why this is permitted: a title and an author list are facts about a publication, not zbMATH’s editorial prose — which is why zbMATH can decline to license its own copy while the fact itself remains free. Crossref places no copyright claim on its metadata and invites reuse.
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. A response carrying a Crossref-supplied title says so, and never states that zbMATH provided a title zbMATH withheld.
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.
Some obvious databases were considered and ruled out, on terms rather than on effort:
Google Scholar offers no API and prohibits automated queries, so there is no lawful route to it. Semantic Scholar carries mixed licences including CC BY-NC, whose non-commercial restriction would not compose with the rest of this corpus. MathSciNet is a subscription service whose terms forbid redistribution. An index that argues about provenance has to account for every field in it.
A few entries reference The Stacks Project, a continuously-updated collaborative reference not indexed by zbMATH. 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. That licence governs copying or modifying the content, which this index does not do.
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.
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 are stated in full here, so nothing on this page depends on a file you cannot open:
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.
MathINsiD is built and maintained by Arnaud Mayeux. Contact: contact@mathinsid.org.
The formalization score, the correctness profile, and the design of this bridge between bibliographic records and formal artifacts are described in:
Arnaud Mayeux, Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge, arXiv:2606.11430. Licensed CC BY 4.0.
Section III of that paper defines the score S(P) and the five correctness classes — certified, corrected, uncorrected, open, untested — that this index stores alongside every score.