Talk:Proof: Difference between revisions

:::: Historically has been almost a hundred years since the advent of formal logic (Boole, Peano, Dedekind, Hilbert, Frege, Russell, Whitehead, Quine, Cantor, Zermelo, Fraenkel, Löwenheim, Skolem, Gödel, Gentzen, Tarski works) in which theorems is just sequences of symbols derivable by rules of inference from axioms and a proof is an algorithm of deriving. And more than fifty years since the advent of сomputability theory and formulation of the Church-Turing thesis and the Curry-Howard correspondence (Church, Kleene, Turing, Gödel, Post, Rosser, Curry works). Type Theory is a further development. [http://video.ias.edu/voevodsky-80th Quoting] Voevodsky mathematical logic is just a combinatorial game, which, of course, can be implemented as software, as proof system suitable for proving any theorems.

 

 

== Huh? ==