[FOM] Current issue of Philosophia Mathematica devoted to mathematical depth

[Timothy Y. Chow]

I read some of the papers in this issues and they were interesting, but I 
agree with what some contributors and cited authors said, which is that 
it's not clear if anything deep can be said about mathematical depth.

If one is interested in constructing some kind of mathematical model of 
depth (or of something like depth), then my feeling is that the most 
promising approach is to define depth in terms of a *prover*.  That is, 
depth shouldn't be a property of a theorem, or even a property that is 
relative to a particular proof of a theorem, but should be a property that 
is relative to a particular general-purpose theorem-prover.  I envisage 
some definition of a prover that has severe time and space constraints but 
has a lot of abbreviation power, and that a theorem would be deep 
*relative to the prover* if

1. the prover cannot find a proof of the theorem within its computational
    constraints, but

2. the theorem admits a proof that the prover can verify, but any such
    proof heavily uses the abbreviation capability.

Unfortunately I don't really see a good way of making precise all the 
vague parts of this proposal.

Tim