Goedel-LM/Lean-workbook-proofs

1,182 downloads in 30 days16 likesLast modified 24 Mar 2025View on Hugging Face

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

Declared licence: Not declared in the tag or the card (see datasets with no declared licence)Evidence: README.md at b731852
Licence files: LICENSE, licence not identifiedEvidence: LICENSE at b731852
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

```latex
@misc{lin2025goedelproverfrontiermodelopensource,
      title={Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving}, 
      author={Yong Lin and Shange Tang and Bohan Lyu and Jiayun Wu and Hongzhou Lin and Kaiyu Yang and Jia Li and Mengzhou Xia and Danqi Chen and Sanjeev Arora and Chi Jin},
      year={2025},
      eprint={2502.07640},
      archivePrefix={arXiv},
      primaryClass={cs.LG},
      url={https://arxiv.org/abs/2502.07640}, 
}
```

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": "Goedel-LM/Lean-workbook-proofs" })
signal: "unclear"
stated_licence: null
sources: 0