AI4Math ChronicleAI4Math 大事记

The QED Manifesto articulates a shared vision for a machine-checked mathematical knowledge base

QED was a field-building vision rather than a single software release, calling for broad cooperation around shared formal mathematical knowledge.

What happened?

The manifesto dated 15 May 1994 proposed the QED project: a computer system representing important mathematical knowledge and techniques with strict formal internal representation and mechanical proof checking.

Why it matters

The manifesto anticipated later large formal libraries, interoperability ambitions and AI systems trained or evaluated over machine-readable mathematics.

Significance rationale: The QED Manifesto articulated a collective vision of representing important mathematical knowledge formally and mechanically checking all proofs, making formalized mathematics a community-scale infrastructure goal.

Historical context

Earlier developments

—

Later developments

—

Related milestones

—

Primary evidence

Evidence & status at a glance

Significance
H2 · Field milestone
Verification
Paper released
Evidence level
E2 · Research record
AI role
Not applicable
Formal assurance
No formal assurance

How should these labels be read? →

Contribution & verification

Mathematical novelty
Not applicable
Interface
Not applicable
AI contribution
The milestone is a community vision and governance document, not an AI system performing mathematics.
Human contribution
The QED community formulated the shared vision for formal mathematical knowledge infrastructure.
Verification
Paper released · E2 · Research record · No formal assurance
Last reviewed
2026-09-15

Technical details

Systems
—
Organizations
—
Problems
—
Methods
—

Sources & artifacts

Verification history

  • 1994-05-15 · Paper released · E2 · Research record

    The dated manifesto directly records the proposed QED project and its goals.

Corrections

No corrections recorded.