Proof assistant Coq allows to represent any theorem as the lambda type (whose proof is the lambda term) (there are other proof assistants like Isabelle/HOL, Lean, etc. that allows similar grammatical tasks). Apparently - there is grammatical procedure to generate all lambda types and it can be done (except for infinities, of course). Apparently there is correspondence between lambda types and theorems and words from the grammar of lambda types. Each word is some theorem. well - there may be details about degrees of infinities, but still.
But not all theorems are of equal importance, there was effort to define the interestingness of the theorems https://www.sciencedirect.com/science/article/abs/pii/S107158190090394X and then use this notion for automatic discovery of interesting theorems and even theories https://www.springer.com/gp/book/9781852336097 by generating words that are intereseting. That was one efforts that seems not developing furtner.
Then there is reverse mathematics https://en.wikipedia.org/wiki/Reverse_mathematics that tries to find axioms necessary to prove the theorems.
What I am trying to say by those two developments is that there are some interesting mathematical concepts, theorems that are very fruitful for the further advancement of the mathematics and the main task of mathematicians is to discover those concepts and theorems. Of course, one can enumerate, generate all theorems but that is not cost efficient way and that is why the focused approach is needed and it is done my mathematicians today.
My question is - what are the formal properties of interestingness of some defintions and theorems as represented as lambda types and terms using grammatical facilities? Are there some grammatical motifs in the interesting terms and types that appears again and again? If lambda term is the proof and if it contains some motif that repeats itself from one term to another, then such motif can signal about existence of some Coq tactic for use in automatic proof? Maybe some motifs in lambda type constructions signal that such lambda type/theorem can be used in the proof in many other theorems? Is there purely combinatorial or grammatical research about interestingness of theorems and concepts that can explain the crowding effects in reverse mathematics (utmost importance of small number of axioms, theorems)?
Maybe combinatorics on words https://en.wikipedia.org/wiki/Combinatorics_on_words can guide use?
There are 2 notions:
- interesting, repeated motifs in the lambda terms (proofs) signal about possible Coq tactic and extraction of such motifs can guide the automated theorem proving, also, generation and exploration of such motifs can explain the value of tactics and generate new tactics by purely grammatical tools;
- interesting, repeated motifs in the lambda types signal about the interestingnes of the theorem and discovery of interesting motifs (and meta-motifs) can be the source generation of interesting, valuable theorems, including algorithms.
One can argue, that mathematics is independent of the language. Of course, but lambda calculus are generic in the ultimate sense - there are only 2 basic types - object (o or i) and truth (t, proposition) and all the other types are constructed from those 2 types by some rules, there is nothing more. So - the Coq representation of the math is suitable for such endeavours.
Of course, I am aware of the discussion About a question on formalising "interestingness" in mathematics (unfortunately, I have not seen the deleted question), but my current question is not about aesthetics and philosophy (why?), it is about grammar and motifs (what?) and some explanation why such motifs can work. And my question contains references to the work of S. Colton and recursive mathematics for which such crowding around axioms is open question, as I understant. Maybe grammatical tools can insight into reverse mathematics?
I would be glad to research this question, but I would like to know the status quo, some references in this direction of thought.