Talk:Proof: Difference between revisions

::::::::# Give the proof of the theorem in such a way that it can be mechanically verified - in a finite amount of time - to be a valid proof by the compiler (e.g. encoded as a program that has the required type encoding the theorem.)

:::::::: The Agda, Coq and Twelf solutions do precisely this. The Omega solution does as well, if one is convinced this solution restricts itself to a sound subset of language. I don't quite follow the J sample but it seems to add a small number of even number and verifies that they are in fact even (one counterexample is enough to disprove a theorem, any finite number of examples are not enough to demonstrate a property holds for all natural numbers.) It doesn't seem to "Define a type of even numbers (0, 2, 4, 6, ...) within the previously defined range of natural numbers." as requested by the task. —''[[User:Ruud Koot|Ruud]]'' 16:44, 10 May 2012 (UTC)