viai957/lean-prover-data

113 downloads in 30 days0 likesLast modified 20 Oct 2026View on Hugging Face

The declared licence (cc-by-sa-4.0) is classified as share-alike.

Declared licence: cc-by-sa-4.0, from the tagEvidence: README.md at 4058f68
Licence files: No licence file at the top level of the repositoryEvidence: file list at 4058f68
Declared sources: None listed in the card metadata
Access gated on Hugging Face: No

Each cell links to what was checked: a file, a file list or a Hub record.

Citation text from the card

The repository as a whole is released under **CC-BY-SA-4.0**. The reason is that some files, notably
`supply_v1.jsonl`, `screen_v1.jsonl` and their derivatives, contain rows derived from
**nvidia/Nemotron-Math-Proofs-v1 (CC-BY-SA-4.0, © NVIDIA)**.

Rows from the other sources keep their original permissive licenses:

| Source | License |
|---|---|
| Goedel-LM/Goedel-Pset-v1 | MIT |
| HangHor/RL-Goedel-Pset-Level-4-5 | MIT |
| SphereLab/FormalMATH-All | MIT |
| STP Lean | MIT |
| iiis-lean/NuminaMath-LEAN-Sol | Apache-2.0 |
| NuminaMath-LEAN | Apache-2.0 |
| Lean Workbook | Apache-2.0 |
| Herald statements | Apache-2.0 |
| Kimina prompt set | Apache-2.0 |
| google-deepmind formal-conjectures | Apache-2.0 |
| miniF2F | MIT |
| ProofNet# | MIT |
| MOBench / compfiles | its upstream license |

Model outputs are from Goedel-LM/Goedel-Prover-V2-8B (Apache-2.0).

The miniF2F, ProofNet and MOBench files are **evaluation data**. Do not train on them.

All datasets marked Permissive or share-alike | JSON

The same facts for your agent

A free MCP server at mcp.datalicense.uk/mcp. Connect it from an MCP client such as Claude or Cursor.

dataset_licence({ "id": "viai957/lean-prover-data" })
signal: "permissive"
stated_licence: "cc-by-sa-4.0"
sources: 0