Edinburgh Research Explorer

Automated theorem provers: a practical tool for the working mathematician?

Research output: Contribution to journalArticlepeer-review

Related Edinburgh Organisations

Open Access permissions



Original languageEnglish
Pages (from-to)3-14
Number of pages12
JournalAnnals of Mathematics and Artificial Intelligence
Issue number1
Publication statusPublished - Jan 2011


In contrast to the widespread use of computer algebra systems in mathematics automated theorem provers have largely met with indifference. There are signs that this is at last beginning to change. We argue that it is inevitable that automated provers will be adopted as a practical tool for the working mathematician. Mathematical applications of automated provers raises profound challenges for their developers.

    Research areas

  • Automated theorem proving, Mathematician's assistant, Very large proofs, Proof understanding

Download statistics

No data available

ID: 416031