Over 400,000 proof method applications from the Archive of Formal Proofs, each with over 100 extracted features. The dataset was created by Yutaka Nagashima at Universität Innsbruck to facilitate machine learning for theorem proving. It is formatted for easy use by practitioners without expertise in formal logic.
Use Cases
- Predicting proof methods in Isabelle/HOL based on extracted features.
- Training models for automated theorem proving assistance using the described features.
- Benchmarking machine learning tools on a structured logic-based task.
Strengths
- Contains data on over 400,000 proof method applications.
- Includes over 100 extracted features for each application.
- Formatted for easy processing without knowledge of formal logic.
Limitations
- Column-level documentation is absent; field semantics must be inferred after download.
- Row count is unknown, which may limit suitability assessment.
- Last update date is unknown; freshness unverified.
Provenance
- Source
- Archive of Formal Proofs
- Collection Method
- Extracted from proof documents.