Credits
The mathematics here is overwhelmingly other people’s work. What is ours is the submission and verification service around it. Every adapted file keeps its original copyright header and names its authors; where a module was restructured, its page says so.
MathlibApache 2.0
The library everything here rests on. Every definition in this corpus is built from Mathlib, and anything of general mathematical interest belongs upstream in it rather than here.
cslibApache 2.0· 29 modules
Theoretical computer science foundations — rewriting and confluence, labelled transition systems and bisimulation, PAC learning and VC dimension. Adapted and split one concept per module; authors are credited in each file.
formal-conjecturesApache 2.0· 31 modules
Google DeepMind's corpus of formalized open problems. Source of the Jacobian conjecture formalization and of problem statements adapted here.
erdosproblems.comcredited, not vendored
Thomas Bloom's catalogue of Erdős' problems, with references and status for each. Problems adapted here link back to their entry; the scholarship of assembling and maintaining that catalogue is his.
Lean 4Apache 2.0
The proof assistant, and the kernel that decides every verdict on this site. No verdict here is our opinion.
Individual formalizers
Each problem credits whoever formalized its statement and whoever proved it, on that problem’s page. A formalization is a contribution in its own right, and treating it as anonymous infrastructure would be both wrong and self-defeating.
Splitting is not authorship
Much of the adapted work was reorganised — one concept per module, with a human-readable title. That is an editorial change and it transfers no authorship. Where a definition came from elsewhere, the original author is named on the module’s page and in the file.
Something credited wrongly, or not at all? Tell us — we would rather fix it than be right about it.