Coq-MathComp – Dataset by phanerozoic | AlphaNeural AI

You can deploy this model and start earning money today!

phanerozoic/
Coq-MathComp

like

0

text-generation

feature-extraction

theorem-proving

Views

No views yet

Coq-MathComp

Structured dataset from the Mathematical Components library (MathComp) for Coq.

Source

Repository: https://github.com/math-comp/math-comp Commit: 91d97df9cf3204b4dab84f4e24bc633e84b6473d Files: 139 License: other

	Schema

Column Type Description

statement string Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof

proof string Verbatim proof/body, empty if the… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-MathComp.