[MINI] Theorem Provers

Data Skeptic

Episode | Podcast

Date: Fri, 23 Nov 2018 16:09:36 +0000

<p class="p1"><span class="s1">Fake news attempts to lead readers/listeners/viewers to conclusions that are not descriptions of reality.<span class="Apple-converted-space"> </span> They do this most often by presenting false premises, but sometimes by presenting flawed logic.</span></p> <p class="p1"><span class="s1">An argument is only sound and valid if the conclusions are drawn directly from all the state premises, and if there exists a path of logical reasoning leading from those premises to the conclusion.</span></p> <p class="p1"><span class="s1">While creating a theorem does feel to most mathematicians as a creative act of discovery, some theorems have been proven using nothing more than search.<span class="Apple-converted-space"> </span> All the "rules" of logic (like <a href="https://en.wikipedia.org/wiki/Modus_ponens">modus ponens</a>) can be encoded into a computer program.<span class="Apple-converted-space"> </span> That program can start from the premises, applying various combinations of rules to inference new information, and check to see if the program has inference the desired conclusion or its negation.<span class="Apple-converted-space"> </span> This does seem like a mechanical process when painted in this light.<span class="Apple-converted-space"> </span> However, several challenges exist preventing any theorem prover from instantly solving all the open problems in mathematics.<span class="Apple-converted-space"> </span> In this episode, we discuss a bit about what those challenges are.</span></p> <p class="p1"> </p>