# Theorem Proving Task

(Redirected from theorem proving task)

A Theorem Proving Task is a task that requires a formal proof.

**Context:**- It can be solved by a Theorem Proving System (that implements a theorem proving algorithm).

**Example(s):**- "Provide a mathematical proof for mathematical theorem
`M`

”

- "Provide a mathematical proof for mathematical theorem
**Counter-Example(s):****See:**Automated Theorem Proving, Inference Task, Automated Reasoning.

## References

### 2017

- (Wikipedia, 2017) ⇒ https://en.wikipedia.org/wiki/Automated_theorem_proving Retrieved:2017-3-2.
**Automated theorem proving**(also known as**ATP**or**automated deduction**) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

### 2016

- (Alemi et al., 2016) ⇒ Alexander A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, and Josef Urban. (2016). “DeepMath-Deep Sequence Models for Premise Selection.” arXiv preprint arXiv:1606.04442
- ABSTRACT: We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving.