Projects per year
Abstract / Description of output
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.
Keywords / Materials (for Non-textual outputs)
- Automated theorem proving
- Mathematician's assistant
- Very large proofs
- Proof understanding