3 ms·
I believe that these "groupoid" ideas lead into higher category theory, and the supporting mathematics for theorem provers such as Lean.
by Syzygies 4y ago
I believe that these "groupoid" ideas lead into higher category theory, and the supporting mathematics for theorem provers such as Lean.
- peter_d_sherman 4y agoI think you may be right! Also, I think that some of the next breakthroughs for AI might be as follows: 1) Given any Turing-complete computer programming language A, construct a translator to a higher-order intermediate representation, then from that higher-order intermediate representation, construct a translator to programming language B... 2) Do this for all known Turing-complete computer programming languages; 3) Do this for all known Mathematical categories, groups, lemmas, theories, etc., and other Mathematical "objects" (for lack of a better term!) -- in other words, create an intermediate data model "map" (analagous to an intermediate higher-order language used by a transpiler) -- between all of these things in all of Mathematics... Category Theory -- seems like it would be "The next level up"... (Note that I am speculating about most of this(!) -- I claim to be an idiot in [some/many/all] of these areas! <g>)