datalicense

All datasets / florath

florath/coq-facts-props-proofs-gen0-v1

83 downloads in 30 days8 likesLast modified 20 Mar 2024View on Hugging Face
Unclear

The checks could not identify a recognised licence ID in the dataset's metadata.

Declared licence
other, from the tagEvidence: README.md at d8e17b6
Licence files
No licence file at the top level of the repositoryEvidence: file list at d8e17b6
Declared sources
None listed in the card metadata
Access gated on Hugging Face
No
florath/coq-facts-props-proofs-gen0-v1florath/coq-facts-p…other: declared licenceotherdeclared licenceREADME.md ↗no licence file: found at top levelno licence fi…found at top levelfile list ↗
florath/coq-facts-props-proofs-gen0-v1florath/coq-fac…other: declared licenceotherdeclared licenceREADME.md ↗no licence file: found at top levelno licence fi…found at top levelfile list ↗
Each cell links to what was checked: a file, a file list or a Hub record.

Tasks

Citation text from the card

@misc{florath2024enhancing,
      title={Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code}, 
      author={Andreas Florath},
      year={2024},
      eprint={2403.12627},
      archivePrefix={arXiv},
      primaryClass={cs.AI}
}

All datasets marked Unclear | 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": "florath/coq-facts-props-proofs-gen0-v1" })
signal: "unclear"
stated_licence: "other"
sources: 0