[FOM] Unreasonable effectiveness

[Jacques Carette]

On 2013-11-02 11:40 , Timothy Y. Chow wrote:
> I am wondering if anyone else has thought along these lines.  Also I 
> am wondering if there is any plausible way of using the growing body 
> of computerized proofs to make the above outline more precise.  There 
> is of course the problem that the "ontogeny" of computerized proofs 
> does not exactly recapitulate the "phylogeny" of how the theorems were 
> arrived at historically, but nevertheless maybe something can still be 
> done.

At least along these lines, you should dig into the work of Josef Urban 
[1][2] and Cesary Kaliszyk [3][4].  The recent preprint [5] might be of 
particular interest, but they have many papers in this vein.

Jacques

[1] http://cs.ru.nl/~urban/
[2] http://www.informatik.uni-trier.de/~ley/pers/hd/u/Urban:Josef.html
[3] http://cl-informatik.uibk.ac.at/users/cek/
[4] http://www.informatik.uni-trier.de/~ley/pers/hd/k/Kaliszyk:Cezary.html
[5] http://arxiv-web3.library.cornell.edu/abs/1310.2797v1