Automated discovery of interesting theorems by searching motifs in words (e.g. Coq lambda calculus) - grammatical notion of reverse mathematics?
Posted by TomR, at math.stackexchange.com,
Proof assistant Coq allows to represent any theorem as the lambda type (whose proof is the lambda term) (there are other proof…