AI4Math ChronicleAI4Math 大事记

The CADE ATP System Competition institutionalizes head-to-head theorem-prover evaluation

Systems were evaluated in a shared computational environment on standardized theorem-proving problems, making performance comparisons more reproducible and visible.

What happened?

The CADE competition held on 1 August 1996 compared automated theorem-proving systems under common resource limits and problem sets, inaugurating the competition series later known as CASC.

Why it matters

Recurring competitions helped turn automated theorem proving into a benchmark-driven research community with shared evaluation practices.

Significance rationale: The first CADE ATP System Competition created a recurring common evaluation setting for fully automatic theorem provers, reinforcing TPTP-based benchmarking as field infrastructure.

Historical context

Earlier developments

—

Later developments

—

Related milestones

—

Primary evidence

Evidence & status at a glance

Significance
H2 · Field milestone
Verification
Claimed
Evidence level
E2 · Research record
AI role
Computation only
Formal assurance
No formal assurance

How should these labels be read? →

Contribution & verification

Mathematical novelty
Benchmark result
Interface
Formal, Symbolic
AI contribution
Automated theorem provers solved benchmark problems; the Event's primary significance is comparative evaluation and field infrastructure.
Human contribution
Organizers selected problems, defined divisions and resource limits, and ran systems in the common competition environment.
Verification
Claimed · E2 · Research record · No formal assurance
Last reviewed
2026-09-15

Technical details

Systems
casc
Organizations
cade
Problems
automated-theorem-proving
Methods
benchmarking, system-competition

Sources & artifacts

Verification history

  • 1996-08-01 · Claimed · E2 · Research record

    The official FLoC/CADE competition page records the date, entrants and evaluation setup.

Corrections

No corrections recorded.