K05. Human sources

People have written down most of the mathematics that the corpus must hold: in reference works, wikis, textbooks, papers, problem lists, syllabi and exercise banks. This document lists those sources, says what the corpus takes from each one, by which channel, under which licence, and in which order. K06 does the same for the formal libraries.

Each fact about a source has its URL and its date of reading in K01, parts A and B. All counts were read on 2026-10-26, unless the text gives another date. A fact marked "not settled" is in the open questions of K15.

K5.1 What a human source gives

A human source can give five things. Most sources give only some of them:

Every source gives mentions. Only sources of the open class give text. Mentions and locators are the larger part of the value: they fill the inventory (K04), and the inventory is the denominator of the goal. A node can state a theorem in math2's own words from a locator, so a source that gives no text still gives the item.

K5.2 The source document

Each source has one entry in manifests/sources.yaml. A person approves each entry and each change to its licence fields (spec 9.2). The importer reads nothing from a source that has no approved entry.

- id: lebl-ra
  title: Basic Analysis I and II
  authors: [Jiří Lebl]
  kind: textbook            # reference | wiki | textbook | paper-index | extraction | curriculum | exercises | database
  url: https://github.com/jirilebl/ra
  licence: CC-BY-SA-4.0 OR CC-BY-NC-SA-4.0   # SPDX expression, as the source states it
  election: CC-BY-SA-4.0    # for a dual licence: the option that math2 takes
  class: open               # spec 9.3
  licence_read:
    at: https://github.com/jirilebl/ra      # the source itself, never an aggregator
    on: 2026-10-26
    by: <person>
  per_item_licence: false   # true if items have their own licences (K13.4)
  public_domain: null       # or {us: true, eu: true, basis: "..."} (K5.2.3)
  authored: human           # human | ai | mixed (K6.5)
  edition: <tag or edition> # pinned edition, where editions differ in licence
  channel: git              # dump | git | api | bulk | page | catalogue
  snapshot: {commit: <commit>, read: <date>}
  terms:
    robots: <summary or n/a>
    rate: <limit that the importer keeps>
    ai: <clause on AI or machine learning, or "none stated">
  attribution: "Jiří Lebl, Basic Analysis I and II, CC BY-SA 4.0, https://github.com/jirilebl/ra"
  adapter: importer/latexthm
  approved_by: <maintainer>

K5.2.1 Read the licence at the source

The licence of a book or a site is read at the source: the LICENSE file of its repository, its front matter, or the licence page of the site. A catalogue such as the Open Textbook Library or the PreTeXt catalogue is a list of candidates, not a licence. Research B found three stale or simplified licences in the Open Textbook Library in one afternoon (K5.4.2).

The licence is read again at each new snapshot. A change of licence between snapshots changes the class of the new snapshot only. The text that math2 took under the old licence keeps that licence, and the source document keeps both, with the snapshot of each.

K5.2.2 Dual licences

When a source offers a choice of licences, math2 takes the option that the prose zone can hold, and the field election records the choice. Examples: Lebl's three books (CC BY-SA 4.0 or CC BY-NC-SA 4.0), Hefferon's Linear Algebra (GFDL or CC BY-SA 3.0 US), and ProofWiki (CC BY-SA 3.0 and the GFDL). The attribution names the elected licence.

K5.2.3 Public domain

Public domain depends on the country. In 2026, a work published in the United States before 1931 is in the public domain there. In the EU, a work is in the public domain 70 years after the death of its author, so in 2026 the author must have died before 1956. math2 is published in all countries, so:

• A work is open as public domain only when it is in the public domain in the United States and in the EU. The field public_domain records both answers and the basis for each, for example the date of publication and the year of the death of the author.
• A work that is in the public domain in one of them only is record.
• A translation, a modern edition and a modern commentary have their own copyright. The importer takes only the text of the original, from an edition whose added text it does not use. Project Gutenberg texts lose the Project Gutenberg header and licence text, as its licence requires.

Hardy's A Course of Pure Mathematics (Project Gutenberg #38769) passes both tests: it was published before 1931, and Hardy died in 1947.

K5.2.4 The authored field

The field authored of K6.5 applies to human sources too. A source that people wrote is human. A source with parts that a model wrote is mixed, and the source document says which parts. For example, the "slogans" of the TheoremSearch datasets were written by DeepSeek-V3.1, so they are ai, while the statements are from the papers. Text from an ai part counts as agent text for the rules of K07 and K09: it needs the same checks as text that a math2 role wrote.

K5.3 Reference works and wikis

Notes on the table:

• Wikidata formulas. The P2534 count is mostly primes. The importer drops the items that are instances of prime number (Q49008) and its kin before it treats P2534 as a source of formulas.
• Stack Exchange dumps. Since July 2024 the dumps are behind a click-through that excludes the training of large language models. math2 does not train a model on them, but the click-through is a contract, so the importer uses the API and not the dumps. The importer reads only posts that a node cites or that the enumerate role proposes as a source, not whole sites. Each post has its own licence, by date (rule L06).
• Wiki text and the copy check. Text from a wiki that enters a node keeps the licence of the wiki and the attribution of its history. The copy check (K9.4) sees it as a match with an open source. That match is allowed, and it adds the attribution.

K5.4 Open textbooks

Open textbooks are the main source of text for the textbook layer (K2.7). They give statements, proofs, examples and exercises in the order that a course needs, and the theorem environments of their sources mark each item.

K5.4.1 Table A: books that the prose zone can take

Each licence below was read at the source of the book. Each book needs attribution. A CC BY-SA 3.0 Unported text may be adapted under CC BY-SA 4.0 (its §4(b)). For the 3.0 US port of Hefferon, the same clause is assumed and not settled.

The Open Textbook Library lists more books under CC BY or CC BY-SA, for example Zakon, Kuttler, Shimamoto, Petrunin, Callahan and OpenIntro Statistics. They are candidates. Each one enters Table A only after a person reads its licence at the source.

K5.4.2 Table B: books that the prose zone cannot take

These books give mentions, locators, tables of contents and internal embeddings, but no text in nodes.

Three books on this list are often taken to be open: Hatcher, Book of Proof and Axler. They are not open for the prose zone.

K5.4.3 Aggregators

• Open Textbook Library. 214 mathematics books. By its own licence data, about 48% are open. Its licences can be stale or simplified: it lists Active Calculus as CC BY-NC-SA (true for the 2017 edition only), Book of Proof as "Attribution-NoDerivs" (the author says CC BY-NC-ND), and Hefferon as CC BY-SA only (the book is dual-licensed). The corpus uses it as a list of candidates.
• AIM Open Textbook Initiative. 68 approved titles. The list shows no licences. Fourteen titles have licences that nobody has read yet (K15).
• PreTeXt catalogue. 67 mathematics projects. Many have only a badge that says "Creative Commons", with no variant. Each one needs a check at the source.
• LibreTexts. The licence is set page by page, and one book can mix licences. The importer goes to the upstream source of each book. Where it reads LibreTexts, it reads page by page, by the license: tag of each page. A page without a declared licence is record.

K5.4.4 Editions

Some books changed licence between editions: Levin's 4th edition became CC BY-NC-SA, and the OpenStax 2nd editions are CC BY-NC-SA where the 1st editions were CC BY. An earlier edition keeps the licence under which it was published. So the source document of such a book pins the edition and the commit (field edition), and the importer reads nothing from a later commit until a person approves the licence of that commit.

K5.4.5 What the importer takes from an open textbook

From the theorem environments of the source (\begin{theorem}, PreTeXt <theorem>, CNXML <rule>, and the like):

• the kind, the number and the title of each environment, as a mention with a locator;
• the statement, the proof, the examples and the exercises, as text of the record plane under the licence of the book;
• the cross-references between environments, as candidate uses edges;
• the table of contents and the index, as a curriculum (K5.8) and as index terms for K4.7.

The text enters a node only by the importer of open text (K14.4), with the attribution of the book, and the copy check marks it as a match with an open source. The write role does not paste it: a role that writes a node from scratch has no text of a restricted book in its context (K7.5), and it may have open text there, with its licence.

K5.5 Closed textbooks

Most of the standard textbooks are not open. They give records and locators only:

• The record of the book: ISBN, edition, zbMATH and MR ids, from catalogues (K5.6).
• Locators: "Rudin, Principles of Mathematical Analysis, 3rd edition, Theorem 3.14". A locator is a fact.
• The table of contents and the index, where the publisher shows them in public, for example in a preview or on the site of the book. They go into the record plane as one locator for each item, not as a copy of the table (K13.4). An index term is a mention of a definition, and K4.7 uses the index terms of standard books to measure recall.
• Not the text. No text of a closed book enters the record plane, the context of a role, or a node. E2 needs two book locators that a person has checked (spec 9.7), because that check needs the book.

The list of closed textbooks in scope comes from the curricula of K5.8: each book that a syllabus names is a candidate.

K5.6 Literature indexes and full text

The research literature is the record plane of spec 09. This section adds the facts of 2026 that change what the importers do.

Three facts change the plan of spec 09:

1. More of arXiv is open than spec 9.3 says. In a sample of three days of 2026, 36.9% of new mathematics papers were open (CC BY 34.0%, CC0 1.9%, CC BY-SA 1.0%). Spec 9.3 gives about 15%, which is the share of all papers since 1991. The sample is small, so phase 1 measures the share over all of 2026 from the metadata plane, and spec 9.3 then gives both figures.
2. The zbMATH knowledge graph is updated about twice a year, not each month. Its licence is CC BY 4.0 in one field of the Zenodo record and CC BY-SA 4.0 in its description. Both are open, but they differ for derived exports, so the importer treats it as CC BY-SA 4.0 until zbMATH answers (K15).
3. Full-text aggregators do not change the licence of a paper. S2ORC, CORE and the Internet Archive hold texts under the copyright of each paper. An importer takes a text from them only when the licence of that paper allows it.

K5.7 Extraction projects

Spec 9.6 says that math2 aligns to the large extraction projects and does not compete with them. The data of 2026:

The BY-SA release of TheoremSearch is not taken as one block. The importer filters it by source and by the licence of each row, and drops the Stacks rows and every row whose licence is NC or not stated.

K5.8 Curricula and theorem lists

Curricula say which items a course needs, and in which order. The corpus imports them as data (K10.3), never as text:

A curriculum is also a mention source: each item that it names is a mention, with the curriculum as its source. The curriculum term of the priority (K12.3) comes from these mentions. The difference between Mathlib's 100.yaml (78 with declarations) and Wiedijk's count for Lean (83) is not settled.

K5.9 Exercise banks

The large exercise banks have licences that the prose zone cannot take. They give links, and the exercise node (K8.7) is math2's own text:

The exercise role (K7.3) has no text of an NC bank in its context.

K5.10 Channels and politeness

The importers keep each limit below, identify themselves with the User-Agent of the toolchain, m2/<version> (+https://github.com/tamnd/math2-agent), with no personal address, and prefer a dump to live requests:

A source that blocks automatic clients, or asks for a login or a click-through, is not read until a person decides how to proceed. The importer never passes a gate.

K5.11 Adapters

Each source has one adapter, importer/<source>, in tamnd/math2-agent (K12.8). Spec 09.1 puts adapters in internal/ingest/<source>. The corpus uses importer/<source> instead, because the toolchain has no internal/ packages. Most sources share a format, so most adapters are thin and use a format package:

Each adapter has fixtures from a small sample of its source, and tests that use the fixtures and never the network (spec 19). An adapter writes mentions and nothing else (K4.2).

K5.12 The order of import

The order follows K14. A source enters when the phase before it meets its exit:

1. Phase 1, open data with no doubt about the licence. Wikidata, the Mathlib lists, 1000+, OEIS names, π-Base, DaRT, Fungrim, and the records of OpenAlex, Crossref, DataCite, HAL and Numdam. Then the records and locators of the record and gfdl sources: the tags of the Stacks Project and Kerodon, the names of the nLab, the ids of MathWorld and the EoM from Wikidata, the tables of contents of closed textbooks where the publisher shows them.
2. Phase 2, the pilot area (group theory). Wikipedia, ProofWiki, PlanetMath and groupprops for the area, the Table A books that cover it (Judson is gfdl, so it gives locators only), the curricula of K5.8, and the Stack Exchange posts that the nodes cite.
3. Phase 3 and later, the textbook layer. The rest of Table A, the rest of the wikis, and TheoremSearch -permissive and TheoremGraph for the research layer. Each new source first goes through the held-out check of K4.7.

K5.13 Corrections to the main spec

K5.14 Rules

With rules L01 to L07, these rules are the licence gate for human sources. The open questions of this document are in K15: the current licence of the EoM, the terms of Stack Exchange of 13 November 2025, the licences of the nLab and the Manifold Atlas, the knowls of the LMFDB, the zbMATH licence, the 14 AIM titles, the US port of CC BY-SA 3.0, and the sources that the research could not reach.

Markdown · Source · Edit