The Coq mailing list

[Alex Meyer <alex153 AT outlook.lv>]

Coq (and Isabelle, Misar, Lean) can represent theorems as lambda types and their proofs as lambda terms (e.g. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#The_normal_proof_of_(%CE%B2_%E2%86%92_%CE%B1)_%E2%86%92_(%CE%93_%E2%86%92_%CE%B2)_%E2%86%92_%CE%93_%E2%86%92_%CE%B1_in_natural_deduction_seen_as_a_%CE%BB-term ). Are there research efforts to enumarate all such lambda types and terms, and find interesting motifs in types (=interesting theorems) and in terms (=interesting tactics)? Maybe combinatorics on words can be of help here? Maybe combinatorics on words have been applied to the Coq types and terms? There is work of S. Colton in the notions of "interesting theorem" and also recursive mathematics experience that some axioms are very valuable, more valuable than other. Maybe there is grammatical approach for gaining insight and explanation into this. I have open question on stackexchange where I have provided further references https://math.stackexchange.com/questions/3532113/automated-discovery-of-interesting-theorems-by-searching-motifs-in-words-e-g-c .

Maybe Coq grammar can be used for generating interesting theorems (there is this buzz about natural language text generation from the neural networks in the machine learning community. the theorem generation in my question will be both rigorous and guided by the motifs - past successes) and for automated discovery of usable and valuable tactics from existing proofs.

I hope that this is not complete offtopic. I this is offtopic that feel free the delete it and I will not ask similar exploration qustion anymore.

A.