That depends on what you mean by "Church-Turing thesis": * http://www.cse.uconn.edu/~dqg/papers/strong-cct.pdf http://www.cse.uconn.edu/~dqg/papers/strong-cct.

That depends on what you mean by "Church-Turing thesis": * http://www.cse.uconn.edu/~dqg/papers/strong-cct.pdf http://www.cse.uconn.edu/~dqg/papers/strong-cct.pdf The Interactive Nature of Computing: Refuting the Strong Church-Turing Thesis (Published version here: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.455.4770&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.455...) * https://www.semanticscholar.org/paper/Computability-Beyond-Church-Turing-via-Choice-Bickford-Cohen/dfd626bdd64b7722d473ad15e3f327610f2e9288 https://www.semanticscholar.org/paper/Computability-Beyond-C... See also a previous hacker news discussion of the Church-Turing thesis here: https://news.ycombinator.com/item?id=18253994 https://news.ycombinator.com/item?id=18253994 albeit I take issue with the supposed "proof" by counter example via Compass & Straightedge construction given in the video there, due to results like these two: * https://link.springer.com/article/10.1007/s10472-018-9603-0 https://link.springer.com/article/10.1007/s10472-018-9603-0 Kellison, Ariel; Bickword, Mark; Constable, Robert L. - Implementing Euclid’s straightedge and compass constructions in type theory [September 2018] (Code here: http://www.nuprl.org/LibrarySnapshots/Published/Version2/Mathematics/reals!model!euclidean!geometry/index.html http://www.nuprl.org/LibrarySnapshots/Published/Version2/Mat...) * https://geocoq.github.io/GeoCoq/ https://geocoq.github.io/GeoCoq/ (Numerous papers by Michael Beeson et al., just check the page, I won't link them all here) (Note that the authors of the two above works take very different yet similar approaches to the whole matter, it really pays off to compare both to each other.) However, there seem to exist at least two different spanners in the works: * https://link.springer.com/article/10.1007/s10472-018-9610-1 https://link.springer.com/article/10.1007/s10472-018-9610-1 Makowsky, Johann A. - Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries * https://link.springer.com/chapter/10.1007/978-3-662-57669-4_15 https://link.springer.com/chapter/10.1007/978-3-662-57669-4_... Makowsky, Johann A. - The Undecidability of Orthogonal and Origami Geometries (If the first of the two above papers makes you wonder "well who DIDN'T overlook Ziegler's theorem... Well... https://scholar.google.com/scholar?cites=2279217158168053275 https://scholar.google.com/scholar?cites=2279217158168053275) Oh and in case anyone here still believes Hilbert's old wives tale about /his/ Axiom of Choice, there's plenty of AC to go around in constructive mathematics: https://vrahli.github.io/articles/bar-induction-lics-long.pdf https://vrahli.github.io/articles/bar-induction-lics-long.pd... But if that doesn't convince you yet, you might go through the 5 stages of accepting it anyway, as outlined by Andrej Bauer here: * https://mathoverflow.net/questions/25363/au-revoir-law-of-excluded-middle/25385 https://mathoverflow.net/questions/25363/au-revoir-law-of-ex... * Here: https://www.youtube.com/watch?v=21qPOReu4FI https://www.youtube.com/watch?v=21qPOReu4FI * And here: https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016... And here's one last paper to almost conclude what turned into a bit of a larger-than-I-expected Constructivism propaganda piece comment: http://t-news.cn/Floc2018/FLoC2018-pages/preprint_cX1w.pdf http://t-news.cn/Floc2018/FLoC2018-pages/preprint_cX1w.pdf "On Expanding Standard Notions of Constructivity" And to now conclude this, a semi-joke: Wouldn't the fact that one can't prove the Church-Turing thesis, but could falsify it by counterexample, put propagation of belief in the meme of the Church-Turing thesis into either the complexity class of RE, or co-RE? ;)