Na sua mensagem “As origens e motivações das fundações univalentes. Uma missão pessoal para desenvolver verificação de prova computacional para evitar erros matemáticos.” (“The Origins and Motivations of Univalent Foundations. A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes.”) Vladimir Voevodsky escreve:
“… vou supor que qualquer fundação de matemática adequada tanto para a raciocínio humano quanto para a verificação por computador deva ter as seguintes três componentes. A primeira é um sistema de dedução formal: uma linguagem e regras de manipulação de sentenças puramente formais, de modo que o registro destas manipulações possa ser verificado por um programa de computador. A segunda componente é uma estrutura que atribui um significado às sentenças desta linguagem em termos de objetos mentais intuitivamente compreensíveis por seres humanos. A terceira componente é uma estrutura que permite aos seres humanos codificar as ideias matemáticas em termos dos objetos diretamente associados à linguagem.”
O objetivo neste curso é para alunos aprenderem essas três componentes para melhor se basear em matemática.
O curso introduz os alunos para a lógica matemática, metamatemática, fundações de matemática, conjuntos, tipos e categorias, relacionamento de matemática, lógica e programação, e as assistentes de provas tais como Coq e LEAN, as linguagens de programação modernas dedicadas ao programa de formalização e verificação de provas.
O aluno precisa de um computador com um teclado.
O primeiro mes alunos jogam em jogo dos números naturais (Natural Number Game) de Kevin Buzzard, o que é uma gamificação do trabalhos de Grassmann e Peano. Ele serve como uma pre-introdução ao Lean e às provas, está baseado no modo “tático” de provas em LEAN. O objetivo é terminar todos os níveis do jogo. A partir do segundo mes os alunos já escrevem os programas em LEAN e resolvem os problemas das varias fontes, tais como “Lógica e Provas” (ref [2]). A partir do segundo mes os alunos aprendem usar LEAN como uma linguagem e assistente de provas, e aprendem não somente o modo tático, mas também em modo normal, em particular aprendem cálculo lambda. Todas as soluções são verificadas automaticamente pela mesma assistente LEAN. Para obter o grau 10 o aluno tem que resolver todos os problemas atribuídos e colocar no repositório git. Diferentes alunos recebem distintos problemas (sem interseção).
O curso é feito pelo zoom, com alunos compartilhando o seu terminal de jogo, LEAN, etc, contribuindo as suas soluções no respositório de github sergunchik/lean212, e as dicas rápidas pelo bate-papo de LEAN e/ou grupo dedicado de Telegram.
A parte prática do curso está complementada por parte teórica, introduzida por instrutor, em paralelo.
A avaliação é baseado nas resoluções de problemas.
O grau G1 é baseado no porcentagem de níveis no jogo dos números naturais que o aluno alcançou, e adicionais tarefas escritas (i.e. provas em matemática/lógica “não formal” em sentido do programa de formalização de matemática com computadores e assistentes de provas).
O grau G2, em sua vez, esta baseado na porcentagem dos 10 problemas de provas em LEAN resolvidos, que foram atribuídos para cada aluno.