</> Code with Papers by Syntology

Home › Datasets › task › Automated Theorem Proving

Automated Theorem Proving datasets

archive 2025-07-28

8 datasets carry the task tag "Automated Theorem Proving" (the task itself: Automated Theorem Proving), ordered by the archive's paper count. Page 1 of 1: 8 shown of 8. Facet routes are this site's own (the archive records the tag string, not a page).

The archive holds 12,214 dataset rows; 12,172 are listed. 6 are withheld from every listing and count here as vandalised before snapshot (6 with contact-centre spam in the title, 0 with a spam description on a row that has no homepage, no paper and no papers counted; none with more than 1 paper, 0 with a benchmark), listed in withheld.json; 1 listed row carries a vandalised description, withheld on its page. This gate never withholds a row with a homepage or a paper that resolves, and a clean description; the content rules below withhold a row whose name is spam whatever else it carries. The gate is a phrase list: these are the rows it caught, not a claim that the rest is clean. Before that gate, the site's content rules withhold 36 more rows (invite-code, gambling, travel-booking, contact-centre and similar spam in the name or on a row with nothing real behind it); they have no page and are listed in withheld.json.

Filter 51 task tags shown of 3,717, by dataset count; the full filter by modality, task and language is on /datasets

All 12,172 Question Answering 413Semantic Segmentation 347Object Detection 332Image Classification 283Classification 222Text Classification 167Language Modelling 166Text Generation 162Visual Question Answering (VQA) 144Named Entity Recognition (NER) 130Pose Estimation 124Anomaly Detection 119Action Recognition 115Instance Segmentation 111Sentiment Analysis 104Text Summarization 98Domain Adaptation 96Speech Recognition 96Reading Comprehension 95Information Retrieval 932D Object Detection 92Image Retrieval 87Machine Translation 82Relation Extraction 822D Semantic Segmentation 81Natural Language Inference 81Image Captioning 79Image Generation 79Depth Estimation 77Node Classification 75Natural Language Understanding 72Autonomous Driving 70Code Generation 70Object Tracking 693D Object Detection 67Face Recognition 67Link Prediction 67Person Re-Identification 65Data Augmentation 63Multi-Task Learning 593D Reconstruction 58Common Sense Reasoning 56Recommendation Systems 56Video Understanding 56Optical Character Recognition (OCR) 55Graph Classification 54Abstractive Text Summarization 52Emotion Recognition 52Medical Image Segmentation 52Word Embeddings 52Automated Theorem Proving 8

Automated Theorem Proving datasets 1–8 of 8

MiniF2F
MiniF2F is a dataset of formal Olympiad-level mathematics problems statements intended to provide a unified cross-system benchmark for neural theorem proving.
TextsAutomated Theorem Proving
84 papers · 2 benchmarks
Geometry3K
A new large-scale geometry problem-solving dataset - 3,002 multi-choice geometry problems - dense annotations in formal language for the diagrams and text - 27,213 annotated diagram logic forms (literals) - 6,293 annotated text logic forms…
ImagesTextsQuestion AnsweringSemantic ParsingMathematical Question AnsweringMath Word Problem SolvingAutomated Theorem Proving
45 papers · 1 benchmark
ProofNet
ProofNet is a benchmark for autoformalization and formal proving of undergraduate-level mathematics.
TextsRetrievalAutomated Theorem Proving
27 papers · 0 benchmarks
MED (Monotonicity Entailment Dataset)
MED is a new evaluation dataset that covers a wide range of monotonicity reasoning that was created by crowdsourcing and collected from linguistics publications.
TextsNatural Language InferenceAutomated Theorem ProvingData Augmentation
18 papers · 1 benchmark
HolStep
HolStep is a dataset based on higher-order logic (HOL) proofs, for the purpose of developing new machine learning-based theorem-proving strategies.
Automated Theorem ProvingMathematical ProofsDimensionality Reduction
10 papers · 2 benchmarks
Kinship
This relational database consists of 24 unique names in two families (they have equivalent structures).
GraphsKnowledge GraphsAutomated Theorem ProvingInductive logic programming
10 papers · 0 benchmarks
HOList
The official HOList benchmark for automated theorem proving consists of all theorem statements in the core, complex, and flyspeck corpora.
TextsAutomated Theorem Proving
8 papers · 1 benchmark
GamePad Environment
GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant.
Automated Theorem Proving
1 paper · 0 benchmarks

Paper counts and descriptions are the archive's, frozen 2025-07-28; no citation counts, no stars, no trending. Sorting by "most cited" or "newest" was a live-site feature the archive does not carry.