Thèse de Church-Turing
Hypothèse : tout ce qui est intuitivement « effectivement calculable » peut être calculé par une machine de Turing (ou par le lambda-calcul, qui lui est équivalent). Ce n'est pas un théorème démontrable — c'est une définition de ce qu'est « calculable ».
Church et Turing, indépendamment, en 1936. Conséquence : tous les modèles « raisonnables » de calcul (machines de Turing, lambda-calcul, machines à registres, fonctions récursives, automates cellulaires, jeu de la vie de Conway) sont équivalents. Extension moderne : la thèse de Church-Turing forte — toutes les fonctions effectivement calculables sont équivalentes à temps polynomial près. L'informatique quantique met la version forte à l'épreuve (l'algorithme de Shor factorise en temps polynomial, ce qu'aucune méthode classique connue ne sait faire).