# Theorem Proving in Large Formal Mathematics as an Emerging AI Field

Preprint · Josef Urban, Jiri Vyskocil

- Archive id: arxiv:1209.3914
- Published: 2012-09-18
- arXiv: https://arxiv.org/abs/1209.3914
- Citations: 0
- Source URL: https://arxiv.org/abs/1209.3914
- PDF: https://arxiv.org/pdf/1209.3914
- Provenance: arxiv

## Abstract

In the recent years, we have linked a large corpus of formal mathematics with automated theorem proving (ATP) tools, and started to develop combined AI/ATP systems working in this setting. In this paper we first relate this project to the earlier large-scale automated developments done by Quaife with McCune's Otter system, and to the discussions of the QED project about formalizing a significant part of mathematics. Then we summarize our adventure so far, argue that the QED dreams were right in anticipating the creation of a very interesting semantic AI field, and discuss its further research directions.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

Topics: [AI for Mathematics & Formal Proof](https://space-kitty.com/topics/ai-mathematics)

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.