Proof Assistants at the interplay of mathematical cultures: a semiotic-cultural analysis of proof in higher education

Nel mondo della matematica universitaria, l'atto di dimostrare un enunciato è più di una semplice risoluzione di un problema; è una pratica culturale. È un modo specifico di pensare, scrivere e validare idee che gli studenti devono apprendere nel passaggio dalla scuola superiore all'istruzione superiore. Per decenni, gli educatori hanno osservato gli studenti lottare per colmare il divario tra gli argomenti intuitivi e informali appresi in precedenza e gli standard rigidi ed espliciti richiesti all'università. Recentemente, un nuovo strumento è entrato in questo panorama: l'assistente alla dimostrazione (proof assistant). Si tratta di programmi informatici progettati per verificare gli argomenti matematici con assoluta precisione, costringendo chi scrive a non lasciare alcun passaggio non spiegato. Mentre alcuni vedono in questi strumenti un modo per rendere la matematica più rigorosa, altri temono che possano soffocare la creatività o confondere gli studenti che sono già in difficoltà. La questione non è semplicemente se questi programmi aiutino o ostacolino, ma come cambino la natura stessa del modo in cui una dimostrazione viene scritta e compresa.

Un team di ricercatori di due università francesi ha deciso di esaminare da vicino questa interazione. Non si sono limitati a chiedere se gli studenti imparassero meglio; hanno osservato come il programma informatico rimodellasse il processo di pensiero degli studenti. Lo studio si è concentrato su un corso del primo anno in cui gli studenti utilizzavano un tipo specifico di assistente alla dimostrazione chiamato Verbose Lean. A differenza dei normali linguaggi di programmazione che sembrano codice, Verbose Lean permette agli studenti di scrivere in una forma controllata di linguaggio naturale, rendendolo più simile al modo in cui i matematici parlano e scrivono su carta. I ricercatori hanno osservato una coppia di studenti lavorare su un classico problema: dimostrare che se una sequenza di numeri si avvicina sempre di più a un valore positivo, i numeri in quella sequenza dovranno inevitabilmente diventare positivi essi stessi. Registrando le conversazioni degli studenti, i loro scarabocchi sulla carta, la loro digitazione sullo schermo e il feedback del computer, i ricercatori hanno creato una mappa dettagliata di come un'idea matematica viaggi da un pensiero grezzo a un fatto verificato dal computer.

Ciò che i ricercatori hanno scoperto è che il computer non si limitava a controllare la risposta finale; agiva come uno specchio, rivelando assunzioni nascoste che gli studenti solitamente danno per scontate. In una normale classe di matematica, uno studente potrebbe saltare piccoli dettagli o fare affidamento su una "sensazione" che un passaggio sia ovvio. Il computer, tuttavia, esige che ogni singolo oggetto, ogni condizione e ogni salto logico sia esplicitamente nominato e giustificato. Lo studio ha dimostrato che questo requisito impone una sorta di cambiamento culturale. Gli studenti dovevano tradurre le loro idee fluide e intuitive in una struttura rigida che la macchina potesse comprendere. Questo processo non è stato fluido. Ha comportato un continuo scambio tra gli appunti cartacei degli studenti, le loro parole parlate, i messaggi di errore del computer e le spiegazioni dell'insegnante.

I ricercatori hanno tracciato un'espressione matematica specifica che appariva costantemente nel lavoro degli studenti. All'inizio, gli studenti trattavano questa espressione come un numero utile da usare nel loro ragionamento. Tuttavia, quando hanno provato a digitarla nel computer, il programma l'ha rifiutata. Il computer non ha detto che il numero fosse matematicamente errato; ha detto che il numero era nel posto sbagliato. Gli studenti avevano cercato di usarlo come un'etichetta per una posizione in una sequenza, ma il computer richiedeva un numero intero per quel ruolo, mentre la loro espressione era una frazione. Questo momento è stato un punto di svolta. Ha costretto gli studenti a rendersi conto che, nel mondo dell'assistente alla dimostrazione, il ruolo che un numero gioca è importante quanto il numero stesso. Hanno dovuto ripensare la loro strategia, spostando l'espressione da una parte all'altra del loro argomento, dove finalmente si inseriva nelle rigide regole del computer.

Questa lotta non è stata risolta dal solo computer. L'insegnante, lavorando alla lavagna nella stessa aula, ha disegnato un diagramma per spiegare il concetto visivamente. Ha descritto una "finestra" di una certa dimensione che aiutava gli studenti a capire perché il loro numero dovesse essere più piccolo del valore bersaglio. Questa spiegazione visiva, combinata con il rifiuto del loro primo tentativo da parte del computer, ha aiutato gli studenti a riorganizzare i loro pensieri. Hanno infine capito che il numero con cui stavano combattendo non era la posizione nella sequenza, ma la dimensione del divario che dovevano misurare. Una volta effettuato questo passaggio, il computer ha accettato il loro argomento. La dimostrazione finale non è stata una linea retta dall'idea alla soluzione; è stata un viaggio complesso in cui il significato di un singolo simbolo cambiava a seconda che venisse parlato, scritto sulla carta, spiegato da un insegnante o controllato da una macchina.

Lo studio suggerisce che gli assistenti alla dimostrazione agiscano come "rivelatori epistemici", un termine usato dagli autori per descrivere strumenti che rendono visibile l'invisibile. Essi rivelano gli "non-pensati" della matematica — quelle parti di una dimostrazione che gli esperti e gli studenti solitamente lasciano non dette perché sembrano ovvie. In una classe tradizionale, queste lacune potrebbero passare inosservate. In una classe con un assistente alla dimostrazione, il computer costringe lo studente a colmare ogni vuoto, esponendo le regole nascoste che governano la validità matematica. I ricercatori sostengono che questo non significhi che il computer sia migliore dell'uomo, o che l'uomo sia migliore del computer. Invece, i due sistemi lavorano insieme per creare un nuovo spazio in cui diversi modi di pensare la dimostrazione collidono e si fondono.

I risultati indicano che l'introduzione di questi strumenti cambia la cultura della dimostrazione nell'istruzione superiore. Non si tratta solo di aggiungere un livello di rigore tecnico; si tratta di riconfigurare il modo in cui gli studenti comprendono cosa significhi avere ragione. Lo studio mostra che gli studenti non imparano semplicemente a scrivere codice; imparano a navigare tra mondi di significato differenti. Devono imparare a tradurre la loro comprensione intuitiva in un linguaggio che una macchina possa verificare, pur ascoltando la spiegazione umana dell'insegnante. I messaggi di errore del computer non sono solo ostacoli; sono segnali che dicono allo studente dove la sua comprensione è incompleta. Obbligando gli studenti a rendere esplicite le loro assunzioni implicite, questi strumenti offrono un'opportunità unica per studiare come la conoscenza matematica venga costruita e validata.

In definitiva, il documento conclude che gli assistenti alla dimostrazione non sono strumenti neutrali. Essi portano con sé idee specifiche su ciò che conta come un argomento valido. Quando gli studenti li utilizzano, non stanno solo imparando la matematica; stanno imparando un nuovo insieme di regole culturali su come pensare e comunicare. I ricercatori suggeriscono che questo spostamento offra un luogo privilegiato per studiare la continuità e le rotture tra il modo in cui la dimostrazione viene insegnata, il modo in cui viene praticata dagli esperti e il modo in cui viene controllata dalle macchine. Il percorso degli studenti in questo studio, dalla loro confusione iniziale al loro successo finale, illustra che imparare a dimostrare con un computer è un processo di traduzione. È un processo in cui il significato di un'idea matematica viene testato, rimodellato e infine stabilizzato attraverso l'interazione tra intuizione umana, guida dell'insegnante e precisione della macchina.