Primary evidence
- AUTOMATH, a language for mathematicsS1 · Primary research · Paper
Automath establishes a language for machine-checkable mathematics
Automath represented definitions, propositions and proofs in a highly explicit typed formal language so a computer could verify the correctness of derivations.
What happened?
N. G. de Bruijn presented Automath as a language for expressing mathematical texts in a form suitable for automatic checking; the 1968 Symposium on Automatic Demonstration provides a precise public anchor for the system's early record.
Why it matters
It helped establish the idea that whole mathematical texts—not only isolated logical formulas—could be represented and mechanically checked.
Significance rationale: Automath was a foundational early effort to encode substantial mathematics in a formal language whose derivations could be checked mechanically, anticipating dependent-type proof assistants and large formal libraries.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Computation only
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Computers checked formally encoded mathematical derivations; proof discovery was not the central AI role.
- Human contribution
- De Bruijn designed the formal language and the methodology for encoding mathematical texts for mechanical checking.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- automath
- Organizations
- eindhoven-university-of-technology
- Problems
- formal-mathematical-knowledge
- Methods
- dependent-types, proof-checking, formalization
Sources & artifacts
- AUTOMATH, a language for mathematicsS1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 1968-12-16 · Paper released · E2 · Research record
TU/e and the Automatic Demonstration proceedings establish the early Automath language and its purpose.
Corrections
No corrections recorded.