[FOM] Automating the formulation of definitions

[Mitchell Spector]

In the various discussions on the automating of mathematics, the focus appears to be on automated 
verification of proofs and, more ambitiously, the automated discovery of proofs.

Arguably an even more difficult endeavor is the formulation of mathematical concepts -- in other 
words, the identification of important definitions.

Imagine that we had a program that could quickly churn out non-obvious theorems of ZFC.  Even so, 
how would we identify theorems of interest when they'd be written directly in the language of ZFC 
with no defined terms?  There would be no way to give any sort of context to the long gibberish-like 
strings of symbols we'd be presented with as theorems.

Doing this today, of course we could set things up in advance to include definitions that are 
considered important now.  But for mathematics to progress, we need to be able to identify new concepts.

If this had been done in the early part of the 20th century, for example, definitions for L or for 
measurable cardinals wouldn't have been included, and important theorems involving those concepts 
would likely have gone unnoticed.  If this were done today, important theorems involving currently 
unidentified mathematical concepts would presumably remain unnoticed in the same way.

One way of attempting to automate the formulation of key definitions would be to develop an 
algorithm that went through a large number of automatically generated proofs and found formulas 
(with only a small number of free variables, but at least one) that appear numerous times as 
subformulas in the proofs.  Those formulas would then be singled out as important concepts and given 
names.  (Clearly we would want to count formulas as the same if they differed only in the names of 
their free variables.)

It would seem that this would also help in the discovery of proofs, since important concepts can be 
viewed as possible hints as to how to proceed.

I'm not an expert in this area, so it could easily be that this is already an active area of 
research and I'm just unaware of it.

Mitchell Spector
E-mail: spector at alum.mit.edu