FrenzyMath/Herald_proofs
This is the proof part of the Herald dataset, which consists of 45k NL-FL proofs. Lean version: leanprover--lean4---v4.11.0 Bibtex citation @inproceedings{ gao2025herald, title={Herald: A Natural Language Annotated Lean 4 Dataset}, author={Guoxiong Gao and Yutong Wang and Jiedong Jiang and Qi Gao and Zihan Qin and Tianyi Xu and Bin Dong}, booktitle={The Thirteenth International Conference on Learning Representations}, year={2025}, url={https://openreview.net/forum?id=Se6MgCtRhz}… See the full description on the dataset page: https://huggingface.co/datasets/FrenzyMath/Herald_proofs.
| Author / organization | FrenzyMath |
|---|---|
| License (as declared) | apache-2.0 |
| Downloads | 192 (as reported by Hugging Face) |
| Likes | 5 |
| Created | 13 February 2025 |
| Last updated at source | 13 May 2025 |
Recent changes
- 16 Oct 2026 Description: This is the proof part of the Herald dataset, which consists of 45k NL-FL proofs. Lean version: leanprover--lean4---v4.11.0 Bibtex citation @inproceedings{ gao2025herald, title={Herald: A Natural Language Annotated Lean 4 Dataset}, author={ → This is the proof part of the Herald dataset, which consists of 45k NL-FL proofs. Lean version: leanprover--lean4---v4.11.0 Bibtex citation @inproceedings{ gao2025herald, title={Herald: A Natural Language Annotated Lean 4 Dataset}, author={
Changes detected by Silytics between refreshes of the source.
More from FrenzyMath
Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 16 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.