ABSTRACT
The characterization problem aims at such a specification. The problem lies in how the checkers are positioned on the board, the reasoning in which current board position is embedded, and what the future consequences of the checkers being in the positions might be. In order for the characterization problem to make sense in checkers, researchers have to situate ourselves within the lived, ongoing work of playing checkers. Similarly, in the study of theorem proving, researchers need to return to the phenomenal work of proving theorems. The work of pairing account and practice is the identifying work of proving theorems and, at the same time, that pairing constitutes the relevant detail of a proof account as an account of the theorem it claims to prove. Wherever mathematical theorem provers turn, they find themselves fully embedded in the lived-work of proving theorems.
