From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4

Nel vasto panorama della matematica, esiste un angolo tranquillo dedicato allo studio di come le cose si sommano nel tempo, particolarmente quando queste oscillano avanti e indietro. Questo è il regno dell'analisi reale, dove i matematici esaminano il comportamento di funzioni che cambiano continuamente. Uno dei puzzle più famosi in questo campo riguarda una specifica curva che sale e scende come un'onda, rimpicciolendosi sempre di più mentre si estende verso l'infinito. La domanda è semplice da formulare ma difficile da risolvere: se si somma l'area sotto questa curva oscillante dal punto di inizio fino al punto più lontano che si possa immaginare, che totale si ottiene? Per oltre un secolo, i matematici hanno conosciuto la risposta, ma dimostrarla rigorosamente senza fare ipotesi nascoste è sempre stato un compito delicato. Questo perché la curva non si assesta abbastanza velocemente perché le regole standard di addizione possano applicarsi direttamente; essa si affida a una precisa cancellazione di aree positive e negative per raggiungere una somma finita. Comprendere questo comportamento è cruciale non solo per la matematica pura, ma anche per la tecnologia che sta alla base della moderna comunicazione, poiché questi stessi schemi oscillanti vengono utilizzati per ricostruire segnali e immagini dai dati grezzi.

Recentemente, due ricercatori, Daniel Goldberg e Antoine Vinciguerra, hanno deciso di affrontare questo classico problema utilizzando un programma informatico progettato per verificare le dimostrazioni matematiche con assoluta certezza. Non si sono limitati a scrivere la soluzione; hanno costruito un argomento logico completo e passo dopo passo all'interno di un sistema software chiamato Lean 4, che agisce come un auditor instancabile che rifiuta di accettare un singolo passaggio a meno che non sia giustificato dalle regole della logica. Il loro obiettivo era formalizzare l'integrale di Dirichlet, il nome dato al calcolo di quella specifica area oscillante, e mostrare come esso si connetta a un insieme più ampio di regole per l'integrazione di funzioni periodiche. La sfida che hanno affrontato era che il modo standard in cui i computer gestiscono il calcolo dell'area, noto come integrale di Lebesgue, non può elaborare direttamente questa particolare curva perché la dimensione totale delle sue oscillazioni è infinita, sebbene l'area netta sia finita. Per aggirare questo problema, i ricercatori hanno dovuto trovare un intelligente percorso alternativo che evitasse il problema dell'infinito pur conducendo alla risposta corretta.

Invece di cercare di forzare il computer ad accettare direttamente l'originale curva oscillante, il team ha prima esaminato una versione modificata della stessa in cui la curva veniva elevata al quadrato. Questa versione al quadrato si comporta molto meglio; la sua area totale è finita e ben comportata, permettendo al computer di calcolarla usando metodi standard. I ricercatori hanno poi dimostrato una specifica relazione tra l'area sotto la curva oscillante originale e l'area sotto questa versione al quadrato. Calcolando prima l'area della curva al quadrato, potevano matematicamente trasferire quel risultato alla problematica originale. Questo approccio ha permesso loro di bypassare le difficoltà della convergenza condizionata, dove l'ordine di addizione è importante, e di arrivare al celebre risultato per cui l'area totale è esattamente la metà del numero pi greco. Questa non era una supposizione o una simulazione; era una dimostrazione rigorosa che il limite dell'area, man mano che il confine si sposta sempre più lontano, converge a questo valore specifico.

Avuto risolto il puzzle principale, il team ha utilizzato i loro nuovi strumenti per esplorare cosa altro potesse essere derivato da esso. Hanno mostrato come questo integrale agisca come un filtro capace di trasformare un'onda continua e fluida in un salto netto, simile a un gradino, un comportamento fondamentale per il modo in cui i segnali digitali vengono elaborati. Hanno anche scoperto e dimostrato una collezione di altre identità che coinvolgono prodotti di queste funzioni oscillanti, mostrando come diverse frequenze interagiscono quando vengono moltiplicate tra loro. Questi risultati non sono semplici curiosità astratte; forniscono la base matematica per comprendere come i segnali possano essere ricostruiti da campioni, un concetto centrale nel teorema di campionamento di Shannon usato nell'elaborazione digitale dell'audio e delle immagini. I ricercatori hanno dimostrato che, comprendendo il comportamento di questi specifici integrali, si può derivare formule precise per come diversi schemi d'onda si combinano e si annullano a vicenda.

Il traguardo finale e forse il più sorprendente del loro lavoro è stata la formalizzazione di una formula scoperta da Nikolai Lobachevsky, un matematico noto soprattutto per il suo lavoro sulla geometria non euclidea. Lobachevsky aveva trovato una regola che permette di calcolare l'area sotto una curva oscillante moltiplicata per un modello ripetitivo, guardando semplicemente una piccola porzione di quel modello. I ricercatori hanno dimostrato che questa regola è valida per qualsiasi funzione continua e ripetitiva che possieda un tipo specifico di simmetria, usando il computer per verificare che la somma infinita delle oscillazioni possa essere ridotta a un semplice calcolo su un breve intervallo. Ci sono riusciti dimostrando che qualsiasi funzione di questo tipo può essere approssimata strettamente da una somma di semplici onde cosmiche, e poiché la regola funziona per ogni singola onda, deve funzionare per l'intera funzione. Questo fornisce una prova verificata dal computer di un'identità generale che era stata precedentemente compresa solo attraverso l'intuizione umana e i metodi tradizionali carta e penna.

Il lavoro di Goldberg e Vinciguerra dimostra che anche verità matematiche secolari possono beneficiare della precisione della moderna verifica informatica. Scomponendo il problema in parti gestibili e navigando attorno agli ostacoli che confondono i metodi di integrazione standard, essi hanno creato una solida base per la ricerca futura nell'elaborazione dei segnali e nell'analisi armonica. La loro formalizzazione conferma che l'integrale di Dirichlet è effettivamente il limite delle aree su intervalli limitati e stabilisce un quadro affidabile per la formula di Lobachevsky. Questo traguardo suggerisce che approcci altrettanto rigorosi potrebbero essere applicati a versioni più complesse di questi integrali, portando potenzialmente a nuove intuizioni su come comprendiamo le strutture matematiche che governano il mondo fisico. Il loro articolo è una testimonianza del potere di combinare una profonda intuizione matematica con la logica inflessibile della verifica informatica, trasformando un classico enigma in un fatto verificato.