Terne pitagoriche monocromatiche e meccanizzazione della Matematica

Un famoso problema, posto da R. Graham, chiedeva se sia possibile colorare gli interi positivi con due colori (ad esempio, rosso e blu), in modo tale che non esista alcuna terna pitagorica monocromatica, cioè, nessuna tripla $a, \,b, \, c$ di interi dello stesso colore e tali che $a^2+b^2=c^2$.

Nel 2016, la questione venne risolta in senso negativo da tre informatici, M. Heule, O. Pullman e V. Marek, i quali dimostrarono il seguente risultato [HPM16]:

Teorema. Esiste una bi-colorazione di $\{1, \ldots, 7824\}$ che non contiene nessuna terna pitagorica monocromatica. Invece, non esiste nessuna tale bi-colorazione per $\{1, \ldots, 7825\}$.

La dimostrazione di questo enunciato è stata ottenuta utilizzando in modo essenziale il calcolatore. Più precisamente, i tre autori hanno costruito, per ogni $n$, una formula preposizionale che descrive una bi-colorazione di $\{1, \ldots, n\}$ senza terne pitagoriche monocromatiche. Successivamente, hanno implementato questa formula in un software specificamente progettato per la Logica Matematica (‘’SAT solver’’), cercando soluzioni per specifici valori di $n$.

Per $n=7824$ la ricerca è stata coronata da successo, e il software ha fornito una bi-colorazione esplicita che risolve il problema. Per $n=7825$, invece, nessuna tale colorazione è stata trovata.

Ovviamente, nel caso “negativo”, è rischioso accettare il responso del computer come una dimostrazione rigorosa della non-esistenza di una soluzione. Infatti, bisogna innanzitutto essere sicuri che l’algoritmo sia corretto ed esaustivo e che la macchina funzioni perfettamente; inoltre, molti matematici non sono pronti a considerare come soddisfacente una dimostrazione di impossibilità che non possa essere verificata “a mano’’ (si ricordi il famoso caso del Teorema dei Quattro Colori).

Heule, Pullman e Marek hanno dunque deciso di codificare la dimostrazione per mezzo di un procedimento di “validazione formale del risultato”, che ha prodotto un certificato di 68 gigabyte, che che è stato reso pubblicamente disponibile e contiene abbastanza informazioni per permettere a chiunque (almeno in linea di principio) di riprodurre la dimostrazione.

Questo esempio mostra che siamo arrivati ad un punto nel quale le dimostrazioni “computer assisted” cominciano a diventare essenziali in Matematica, facendoci riconsiderare (almeno in alcuni casi) il nostro concetto di “dimostrazione rigorosa”. Tutto ciò apre scenari affascinanti, e per certi versi inquietanti, sulla “meccanizzazione della Matematica”, che sarebbe troppo lungo considerare qui; il lettore interessato può leggere ad esempio [Av18].

Riferimenti.

[HPM16] M. Heule, O. Pullman e V. Marek: Solving and verifying the Boolean Pythagorean Triples via Cube-an-Conquerer, arXiv:1605.00723.

[AV18] J. Avigad: The Mechanization of Mathematics, Notices AMS 65, number 6 (2018).