All datasets / banach1729

banach1729/goedel-workbook-lean427

1,015 downloads in 30 days0 likesLast modified 22 Mar 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 4049a8c
Licence files: No licence file at the top level of the repositoryEvidence: file list at 4049a8c
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

@article{lin2025goedel,
  title={Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving},
  author={Lin, Yong and Agarwal, Shange and Jiang, Bohan and Lu, Changran and Yuan, Yufei and Liu, Hao and Wang, Tongxuan and Ruan, Zhongjian and Zhang, Qingyu and Zeng, Aimin and others},
  journal={arXiv preprint arXiv:2502.07640},
  year={2025}
}

@article{xin2024deepseek,
  title={DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search},
  author={Xin, Huajian and Guo, Daya and Shao, Zhihong and Ren, Zhizhou and Zhu, Qihao and Liu, Bo and Ruan, Chong and Li, Wenda and Liang, Xiaodan},
  journal={arXiv preprint arXiv:2408.08152},
  year={2024}
}

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": "banach1729/goedel-workbook-lean427" })
signal: "permissive"
stated_licence: "apache-2.0"
sources: 0