Dans un système formel F, on se demande si on peut trouver une preuve de l'énoncé math S t.q. le nb de symboles de la preuve < n. Le problème est décidable, il faut chercher la preuve dans tout le code de F dont les cordes (bit-strings) < n (c'est comme...