# HF corpus upload: per-source licensing matrix

This document is the redistribution audit for the public Hugging Face release of
the mathlas document corpus (the texts and metadata that back the served
3,683,428-document index, plus the live findings store). It covers ONLY the
document corpus: the 30 GB embedding matrices (`index_full_dense.npz` and its
quantized sidecars) are build artifacts and are NOT part of this release.

Audited 2026-06-10 against the actual served artifacts:

* `reference/downloads/index_full.meta.jsonl` (3,683,428 records, row-aligned
  to the served dense matrix; this IS the corpus `search_existing_math` serves)
* `reference/downloads/findings.jsonl` (82 `web_added` records, the live
  findings store)

## Per-source record counts (measured, not quoted)

Counted with `mathlas.retrieve.corpus.source_key` over every line of the served
meta:

| Source key | Records | Provenance |
|---|---|---|
| arxiv | 1,302,109 | TheoremSearch permissive subset, arXiv papers |
| proofwiki | 23,871 | TheoremSearch permissive subset, ProofWiki |
| stacks | 12,693 | TheoremSearch permissive subset, Stacks Project |
| other | 2,410 | TheoremSearch permissive subset, open textbooks (CRing, Open Logic, HoTT Book, Stacks and Moduli, Napkin) |
| dolma | 2,342,345 | Our own extraction from Dolma v1.7 arXiv, slogans generated by us |
| total | 3,683,428 | |

Plus the findings store: 82 `web_added` records (our own annotations with
short quoted statements and full source URLs).

## Licensing matrix

| Upload config | Records | Upstream packaging | Upstream license | Underlying content | Verdict |
|---|---|---|---|---|---|
| `theoremsearch` | 1,341,083 | `uw-math-ai/theorem-search-dataset` (Hugging Face) | CC BY-SA 4.0 (dataset card) | Papers individually permissive: CC BY 4.0 (186,338 papers), CC BY-SA 4.0 (11,587), CC0 (8,456), CC BY 3.0 (2,366), public domain (662), unrecorded (368) of 209,777 papers. Sub-sources keep their own terms: Stacks Project (GNU FDL), ProofWiki (CC BY-SA 3.0), HoTT Book / Open Logic / CRing / Napkin (open textbook licenses). | SHIPS. Redistributed under CC BY-SA 4.0 with attribution to UW Math AI Lab and the original sources. The per-paper `license` value from `paper.parquet` is NOT duplicated into our rows; users needing per-paper terms join on the upstream dataset. |
| `dolma` | 2,342,345 | Statements: short theorem-environment excerpts extracted by us from `emozilla/dolma-v1_7-arxiv` (a mirror of the AI2 Dolma v1.7 arXiv slice). Slogans: generated by us with a local open-weight LLM (Qwen3.6-35B-A3B). | Dolma: ODC-BY 1.0 | The underlying arXiv papers are mostly under the arXiv non-exclusive license (no blanket redistribution right for full texts). What we redistribute is NOT full texts: each record is one short theorem statement (a brief excerpt already redistributed inside the open Dolma corpus) plus our own NL slogan. | SHIPS. Statements under ODC-BY 1.0 attribution (AI2 Dolma); slogans are our own derivatives, released CC BY 4.0. The card states the excerpt nature honestly and notes that paper copyright remains with the authors. |
| `findings` | 82 | Our own live-corpus records (`add_finding`), written by us during web-augmented research sessions. | n/a (ours) | Each record: our NL slogan + a short quoted statement + the full source URL (mostly arXiv abs pages). Embedded `dense_vec` vectors are STRIPPED before upload (embeddings are out of scope). | SHIPS. Our text under CC BY 4.0; quoted statements are brief excerpts with full provenance. |

### Explicitly NOT in the release

| Artifact | Why excluded |
|---|---|
| `index_full_dense.npz`, `.q8.npy`, `.qbin.npy`, BM25 cache | Embedding matrices and serving artifacts, out of scope by design (this release is the document corpus). |
| `reference/downloads/datasets/test_targets/` (3,496 arXiv theorem envs from 61 papers) | Fetched from arXiv source regardless of license for LOCAL benchmark use only; per-paper copyright; NOT redistributable. Never part of the served corpus. |
| `reference/downloads/datasets/arxiv_math/` (117k OAI-PMH metadata) | Benchmark-only slice, not part of the served corpus. (Metadata itself is CC0, but there is nothing to gain by shipping it here.) |
| mathlib slice (`reference/downloads/datasets/mathlib/`) | Apache-2.0 and shippable in principle, but it is not in the served dense corpus (formal search is served live via Loogle/LeanSearch), so it is out of scope. |
| `theorems-test.parquet` (110 human queries) | Upstream evaluation data; users should take it from `uw-math-ai/theorem-search-dataset` directly so ground truth stays canonical. |
| `index_full.meta.jsonl.bak`, `index_full_dense.npz.bak`, `statement_channel/` partials | Superseded or in-progress build artifacts. |

## Verdict

Everything in the served 3.68M corpus plus the findings store is redistributable
and SHIPS. Nothing in the served corpus has to be excluded:

* The TheoremSearch subset is exactly the slice UW released BECAUSE it is
  permissively licensed (their full 9.2M corpus is ~85% non-redistributable
  arXiv-license papers; they withheld those, we never had them).
* The Dolma slice redistributes short excerpts of an already-open ODC-BY corpus
  plus our own generated slogans.
* The findings are our own records once the embedded vectors are stripped.

One correction to earlier internal docs: `docs/05_open_dataset.md` and README
described the TheoremSearch subset as "CC-BY / CC0". That describes the
underlying papers (mostly CC BY 4.0 plus CC0 and friends); the dataset-level
license of the upstream HF card is CC BY-SA 4.0, and that is the license our
`theoremsearch` config inherits and declares.

The HF dataset card therefore declares: `license: [cc-by-sa-4.0, odc-by,
cc-by-4.0]` with this per-source matrix reproduced in the card body.

## Attribution required in the card (and honored)

* UW Math AI Lab, TheoremSearch dataset (`uw-math-ai/theorem-search-dataset`,
  arXiv:2602.05216)
* Allen Institute for AI, Dolma v1.7 (ODC-BY), via the `emozilla/dolma-v1_7-arxiv`
  mirror
* The Stacks Project (stacks.math.columbia.edu, GNU FDL)
* ProofWiki (proofwiki.org, CC BY-SA 3.0)
* Original paper authors (links preserved per record in the `source` field)