Tonic/MiniF2F

122 downloads in 30 days9 likesLast modified 5 Feb 2025View on Hugging Face

The declared licence (mit) is classified as permissive.

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

Citation text from the card

@inproceedings{
  2210.12283,
  title={Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs},
  author={Albert Q. Jiang and Sean Welleck and Jin Peng Zhou and Wenda Li and Jiacheng Liu and Mateja Jamnik and Timothée Lacroix and Yuhuai Wu and Guillaume Lample},
  booktitle={Submitted to The Eleventh International Conference on Learning Representations},
  year={2022},
  url={https://arxiv.org/abs/2210.12283}
}

@article{lin2024Goedelprover,
      title={Goedel-Prover: A New Frontier in 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},
}

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": "Tonic/MiniF2F" })
signal: "permissive"
stated_licence: "mit"
sources: 0