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

No mundo da matemática universitária, o ato de provar um enunciado é mais do que apenas resolver um problema; é uma prática cultural. É uma forma específica de pensar, escrever e validar ideias que os estudantes devem aprender à medida que transitam do ensino médio para o ensino superior. Durante décadas, educadores observaram estudantes lutarem para preencher a lacuna entre os argumentos intuitivos e informais que aprenderam anteriormente e os padrões rígidos e explícitos exigidos no nível universitário. Recentemente, uma nova ferramenta entrou neste cenário: o assistente de prova. Estes são programas de computador projetados para verificar argumentos matemáticos com precisidade absoluta, forçando o escritor a não deixar nenhum passo sem explicação. Enquanto alguns veem essas ferramentas como uma forma de tornar a matemática mais rigorosa, outros temem que elas possam sufocar a criatividade ou confundir estudantes que já estão enfrentando dificuldades. A questão não é simplesmente se esses programas ajudam ou atrapalham, mas como eles mudam a própria natureza de como uma prova é escrita e compreendida.

Uma equipe de pesquisadores de duas universidades francesas decidiu observar de perto essa interação. Eles não apenas perguntaram se os alunos aprendiam melhor; eles observaram como o programa de computador remodelou o processo de pensamento dos estudantes. O estudo focou em um curso do primeiro ano onde os alunos usavam um tipo específico de assistente de prova chamado Verbose Lean. Ao contrário das linguagens de programação padrão que se parecem com código, o Verbose Lean permite que os alunos escrevam em uma forma controlada de linguagem natural, fazendo com que pareça mais próximo da maneira como os matemáticos falam e escrevem no papel. Os pesquisadores observaram uma dupla de estudantes trabalhando em um problema clássico: provar que, se uma sequência de números se aproxima cada vez mais de um valor positivo, os números nessa sequência devem eventualmente tornar-se positivos por si mesmos. Ao registrar as conversas dos alunos, seus rabiscos no papel, sua digitação na tela e o feedback do computador, os pesquisadores criaram um mapa detalhado de como uma ideia matemática viaja de um pensamento bruto para um fato verificado pelo computador.

O que os pesquisadores descobriram foi que o computador não apenas verificava a resposta final; ele agia como um espelho, revelando suposições ocultas que os alunos geralmente dão como certas. Em uma aula de matemática normal, um aluno pode pular pequenos detalhes ou confiar em um "sentimento" de que um passo é óbvio. O computador, no entanto, exige que cada objeto, cada condição e cada salto lógico seja explicitamente nomeado e justificado. O estudo mostrou que esse requisito força um tipo de mudança cultural. Os alunos tiveram que traduzir suas ideias fluidas e intuitivas em uma estrutura rígida que a máquina pudesse entender. Esse processo não foi suave. Envolveu um constante vai e vem entre as notas de papel dos alunos, suas palavras faladas, as mensagens de erro do computador e as explicações do professor.

Os pesquisadores rastrearam uma expressão matemática específica que apareceu ao longo do trabalho dos alunos. A princípio, os alunos trataram essa expressão como um número útil para usar em seu raciocínio. No entanto, quando tentaram digitá-la no computador, o programa a rejeitou. O computador não disse que o número estava matematicamente errado; disse que o número estava no lugar errado. Os alunos haviam tentado usá-lo como um rótulo para uma posição em uma sequência, mas o computador precisava de um número inteiro para esse papel, enquanto a expressão deles era uma fração. Esse momento foi um ponto de virada. Forçou os alunos a perceberem que, no mundo do assistente de prova, o papel que um número desempenha é tão importante quanto o próprio número. Eles tiveram que repensar sua estratégia, movendo a expressão de uma parte de seu argumento para outra, onde ela finalmente se ajustasse às regras estritas do computador.

Essa dificuldade não foi resolvida pelo computador sozinho. O professor, trabalhando no quadro negro na mesma sala de aula, desenhou um diagrama para explicar o conceito visualmente. Ele descreveu uma "janela" de tamanho que ajudava os alunos a entender por que o número deles precisava ser menor que o valor alvo. Essa explicação visual, combinada com a rejeição do computador à primeira tentativa deles, ajudou os alunos a reorganizar seus pensamentos. Eles eventualmente perceberam que o número com o qual estavam lutando não era a posição na sequência, mas o tamanho da lacuna que precisavam medir. Uma vez que fizeram essa mudança, o computador aceitou o argumento deles. A prova final não foi uma linha reta do ídea à solução; foi uma jornada complexa onde o significado de um único símbolo mudava dependendo de se estava sendo falado, escrito no papel, explicado por um professor ou verificado por uma máquina.

O estudo sugere que os assistentes de prova atuam como "reveladores epistêmicos", um termo que os autores usam para descrever ferramentas que tornam o invisível visível. Eles revelam os "não-pensamentos" da matemática — as partes de uma prova que especialistas e estudantes geralmente deixam sem dizer por parecerem óbvias. Em uma sala de aula tradicional, essas lacunas poderiam passar despercebidas. Em uma sala de aula com um assistente de prova, o computador força o aluno a preencher cada lacuna, expondo as regras ocultas que governam a validade matemática. Os pesquisadores argumentam que isso não significa que o computador seja melhor que o humano, ou que o humano seja melhor que o computador. Em vez disso, os dois sistemas trabalham juntos para criar um novo espaço onde diferentes formas de pensar sobre a prova colidem e se fundem.

As descobertas indicam que a introdução dessas ferramentas altera a cultura da prova no ensino superior. Não se trata apenas de adicionar uma camada de rigor técnico; trata-se de reconfigurar como os alunos entendem o que significa estar certo. O estudo mostra que os alunos não aprendem simplesmente a escrever código; eles aprendem a navegar entre diferentes mundos de significado. Eles devem aprender a traduzir sua compreensão intuitiva para uma linguagem que uma máquina possa verificar, enquanto também ouvem a explicação humana do professor. As mensagens de erro do computador não são apenas obstáculos; são sinais que dizem ao aluno onde sua compreensão está incompleta. Ao forçar os alunos a tornar suas suposições implícitas explícitas, essas ferramentas oferecem uma oportunidade única de estudar como o conhecimento matemático é construído e validado.

Por fim, o artigo conclui que os assistentes de prova não são ferramentas neutras. Eles carregam consigo ideias específicas sobre o que conta como um argumento válido. Quando os alunos os utilizam, não estão apenas aprendendo matemática; estão aprendendo um novo conjunto de regras culturais sobre como pensar e se comunicar. Os pesquisadores sugerem que essa mudança oferece um lugar privilegiado para estudar a continuidade e as rupturas entre a maneira como a prova é ensinada, a maneira como é praticada por especialistas e a maneira como é verificada por máquinas. A jornada dos alunos neste estudo, desde sua confusão inicial até o sucesso final, ilustra que aprender a provar com um computador é um processo de tradução. É um processo onde o significado de uma ideia matemática é testado, remodelado e, finalmente, estabilizado através da interação entre a intuição humana, a orientação do professor e a precisão da máquina.