All datasets / iCogLabs-Dev

iCogLabs-Dev/Mathlib-Normalized-Sexpr

131 downloads in 30 days0 likesLast modified 27 Aug 2026View on Hugging Face

Permissive or share-alike

The declared licence (apache-2.0) is classified as permissive.

Declared licence: apache-2.0, from the tagEvidence: README.md at f44841f
Licence files: No licence file at the top level of the repositoryEvidence: file list at f44841f
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.

Tasks

text-generation

Citation text from the card

This dataset is released under `apache-2.0`. It is derived work, and
both upstream licenses continue to apply to the material they cover:

- **Mathlib 4** is licensed Apache-2.0. Theorem names, tactic text, file
  paths, and every elaborated term in the S-expression columns derive from
  Mathlib at commit `29dcec074de168ac2bf835a77ef68bbe069194c5`. See
  <https://github.com/leanprover-community/mathlib4/blob/master/LICENSE>.
- **LeanDojo** is licensed MIT. The row selection and the `split` /
  `row_index` assignment are inherited unchanged from the LeanDojo
  benchmark, so its notice is reproduced below as MIT requires.

```
MIT License

Copyright (c) 2023 LeanDojo Team

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LI

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": "iCogLabs-Dev/Mathlib-Normalized-Sexpr" })
signal: "permissive"
stated_licence: "apache-2.0"
sources: 0