主要证据
- AUTOMATH, a language for mathematicsS1 · 主要研究来源 · 论文
Automath 建立面向机器检查数学的形式语言
Automath 以高度显式的有类型形式语言表示定义、命题与证明，使计算机能够检查推导的正确性。
发生了什么？
N. G. de Bruijn 将 Automath 提出为一种把数学文本表达成适合自动检查形式的语言；1968 年 Automatic Demonstration Symposium 为其早期公开记录提供了精确时间锚点。
为什么重要？
它推动了“完整数学文本而非孤立逻辑公式也可以形式表示并由机器检查”的理念。
重要性说明：Automath 是把大规模数学编码进可由机器检查推导的形式语言的奠基性早期尝试，预示了依赖类型证明助手与大型形式数学库。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- 仅计算支持
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 计算机负责检查形式编码的数学推导；自动发现证明并非核心 AI 角色。
- 人类贡献
- de Bruijn 设计形式语言及把数学文本编码为可机械检查表示的方法。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- automath
- 机构
- eindhoven-university-of-technology
- 数学问题
- formal-mathematical-knowledge
- 方法
- dependent-types, proof-checking, formalization
全部来源与工件
- AUTOMATH, a language for mathematicsS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
验证历史
- 1968-12-16 · 论文已发布 · E2 · 研究记录
TU/e 与 Automatic Demonstration 会议文献确认了早期 Automath 语言及其目标。
更正
当前没有记录的更正。