I had the impression that the Church-Turing thesis has not been proven, but a recent posting to the Arxiv server claimed otherwise. In partricular, Nachum Dershowitz and Evgenia Falkovic in their extended abstract entitled " A Formalization and Proof of the Extended Church-Turing Thesis " claim that they offer a proof of the Extended Church-Turing Thesis: Every effective algorithm can be efficiently simulated by a Turing machine. Interestingly, this proof uses the notion of classical algorithm which is a time-sequential state-transition system, whose transitions are partial functions on its states. But obviously, this is not an algorithm but something that someone calls a classical algorithm. Now if one has a deep desire to prove the Church-Turing thesis, then she can formulate and prove it inside Eff , that is, the effective topos (see Categorical Logic and Type Theory , p. 402)! In a nutshell, no I don't think this paper is a proof of the CTT.