3 ms·
with AI system it is also hard, you need to have some knowledge graph which would explain what is plane, distance, etc, and map it on some set of axioms, theore
by riku_iki 6y ago
with AI system it is also hard, you need to have some knowledge graph which would explain what is plane, distance, etc, and map it on some set of axioms, theorems, predicates and functions.
- currymj 6y agothis is what Lean and other theorem provers are trying to build. which would be useful whether you have a human operator generating the proofs or some kind of automated system.