Primary evidence
- TPTP HistoryS1 · Primary research · Benchmark
TPTP establishes a shared benchmark library for automated theorem proving
TPTP collected ATP test problems into standardized formats with domain classification and release/version discipline so theorem provers could be tested on comparable inputs.
What happened?
The official TPTP history records the first public TPTP v1.0.0 release on Friday 12 November 1993, containing 2,295 problems across 23 domains.
Why it matters
The library became core infrastructure for automated deduction and later supported system competitions, benchmarking and learning-guided theorem proving.
Significance rationale: TPTP standardized a large public problem library for automated theorem proving, enabling repeatable evaluation and meaningful cross-system comparisons over a shared corpus.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Claimed
- Evidence level
- E3 · Inspectable artifact
- AI role
- Computation only
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- AI and ATP systems are evaluated on the library; the milestone itself is benchmark infrastructure rather than an AI-generated mathematical result.
- Human contribution
- Geoff Sutcliffe, Christian Suttner and contributors curated, normalized and maintained the public problem library.
- Verification
- Claimed · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-15
Technical details
- Systems
- tptp
- Organizations
- —
- Problems
- automated-theorem-proving
- Methods
- benchmarking, standardized-problem-formats
Sources & artifacts
- TPTP HistoryS1 · Primary research · Benchmark · accessed 2026-09-15
- TPTP Problem LibraryArtifact · Benchmark
Verification history
- 1993-11-12 · Claimed · E3 · Inspectable artifact
The official TPTP history and current library make the release chronology and benchmark artifacts directly inspectable.
Corrections
No corrections recorded.