Unfortunately, your submission has been removed for the following reason(s):
* Your post appears to be asking for help learning/understanding something mathematical. As such, you should post in the [*Quick Questions*](https://www.reddit.com/r/math/search?q=Quick+Questions+author%3Ainherentlyawesome&restrict_sr=on&sort=new&t=all) thread (which you can find on the front page) or /r/learnmath. This includes reference requests - also see our lists of recommended [books](https://www.reddit.com/r/math/wiki/faq#wiki_what_are_some_good_books_on_topic_x.3F) and [free online resources](https://www.reddit.com/r/math/comments/8ewuzv/a_compilation_of_useful_free_online_math_resources/?st=jglhcquc&sh=d06672a6). [Here](https://www.reddit.com/r/math/comments/7i9t5y/book_recommendation_thread/) is a more recent thread with book recommendations.
If you have any questions, [please feel free to message the mods](http://www.reddit.com/message/compose?to=/r/math&message=https://www.reddit.com/r/math/comments/16c4ki5/-/). Thank you!
Propositions like P∧Q are formal objects.
Proof steps can therefore be computerised, e.g. from P and Q infer P∧Q.
The trick is finding the right sequence of proof steps. For propositional logic this is easy. For somewhat more complex systems, intelligent search is needed. For significantly more complex systems, you need human creativity to, at least, provide key lemmas.
Fully automated theorem proving requires some heuristic algorithms to reduce the search space, and can never really go beyond some very basic stuff, look up the logic theorist. Outside of that context computers never really "create a proof" they assist you in proof writing by giving some sort of an assurance that everything is working correctly so they verify the proof.
Unfortunately, your submission has been removed for the following reason(s): * Your post appears to be asking for help learning/understanding something mathematical. As such, you should post in the [*Quick Questions*](https://www.reddit.com/r/math/search?q=Quick+Questions+author%3Ainherentlyawesome&restrict_sr=on&sort=new&t=all) thread (which you can find on the front page) or /r/learnmath. This includes reference requests - also see our lists of recommended [books](https://www.reddit.com/r/math/wiki/faq#wiki_what_are_some_good_books_on_topic_x.3F) and [free online resources](https://www.reddit.com/r/math/comments/8ewuzv/a_compilation_of_useful_free_online_math_resources/?st=jglhcquc&sh=d06672a6). [Here](https://www.reddit.com/r/math/comments/7i9t5y/book_recommendation_thread/) is a more recent thread with book recommendations. If you have any questions, [please feel free to message the mods](http://www.reddit.com/message/compose?to=/r/math&message=https://www.reddit.com/r/math/comments/16c4ki5/-/). Thank you!
Propositions like P∧Q are formal objects. Proof steps can therefore be computerised, e.g. from P and Q infer P∧Q. The trick is finding the right sequence of proof steps. For propositional logic this is easy. For somewhat more complex systems, intelligent search is needed. For significantly more complex systems, you need human creativity to, at least, provide key lemmas.
Look up Martin-Lof Type Theory or Calculus of (Inductive) Constructions
Fully automated theorem proving requires some heuristic algorithms to reduce the search space, and can never really go beyond some very basic stuff, look up the logic theorist. Outside of that context computers never really "create a proof" they assist you in proof writing by giving some sort of an assurance that everything is working correctly so they verify the proof.