Além do Ensino Médio: Prova, Treinamento Olímpico e Matemática em Nível de Doutorado — O que o “Modo PhD” poderia conter realisticamente

Resultados

(a) O curso de transição para demonstração e pesquisas sobre ensino de demonstrações

A maioria dos departamentos dos EUA insere um curso de “transição para demonstração” entre cálculo e o primeiro curso intensivo em demonstrações (álgebra, análise real) [1]. Sua pedagogia dominante é o método Moore: o instrutor fornece apenas axiomas e uma lista sequenciada de problemas; os estudantes não podem consultar textos, devem provar tudo por conta própria e apresentar uns aos outros [1][2]. As evidências de eficácia são principalmente qualitativas e de longo prazo (mais estudantes ingressando em pesquisa) em vez de estritamente quantitativas [2].

A pesquisa de Selden & Selden faz uma distinção central para o desenho de avaliações: construção de demonstração e validação de demonstração (julgar se o argumento de outra pessoa está correto) são competências separadas, e um curso focado em construção não melhora de forma confiável a validação [3][4]. Estudos de rastreamento ocular e de pensamento-alto mostram que novatos fixam em características superficiais (manipulação algébrica) enquanto especialistas acompanham a estrutura lógica global; a validação é enquadrada como construção ativa de sentido, não como verificação binária — exatamente por isso ela resiste a uma rubrica aplicada por máquina [3][4].

O manejo de quantificadores é a área de falha mais replicada: um estudo com 61 estudantes constatou que nenhum conseguiu reescrever consistentemente uma afirmação informal como seu equivalente formal quantificado correto [1]. Modos de falha recorrentes: não introduzir uma variável ao provar uma afirmação universal; atribuir excessivamente propriedades a uma testemunha existencial; inverter a ordem dos quantificadores (clássico em demonstrações ε-δ); e negar incorretamente uma afirmação (enunciar o “oposto” em vez da negação lógica), o que compromete demonstrações por contradição [5][6]. Um estudo de álgebra linear encontrou estudantes “falando um com o outro” sobre significados diferentes de “único” [6]. Esses são modos de falha discretos e bem definidos — cada um pode ser alvo de um exercício estreito e verificável (veja Implicações de Design).

(b) Como funciona o treinamento para olimpíadas

O treinamento para olimpíadas é organizado em torno de heurísticas + um banco de técnicas, não de um programa linear. How to Solve It (1945), de Pólya, fornece a heurística de quatro estágios — entender, planejar, executar, rever — que sustenta essencialmente toda a literatura de treinamento para competições [7][11]. Problem-Solving Strategies (Springer, 1998), de Engel, voltado a treinadores até nível IMO/Putnam, organiza por técnica (invariantes, princípio da caixa de pombos, princípio extremal, indução, coloração/contagem) em vez de assunto MSC [10][11].

AoPS operacionaliza isso em escala — problemas antes das explicações, currículos do pré-álgebra até MATHCOUNTS/AMC/AIME/ARML e WOOT (treinamento para olimpíadas); todo membro da equipe americana da IMO desde 2015 foi estudante da AoPS [8]. A preparação para o Putnam segue o mesmo modelo orientado por conjuntos de problemas, reforçado por sessões em grupo no estilo de seminário [9][11].

A avaliação em ambos é deliberadamente grosseira e não-aditiva — uma rejeição da pontuação por ponto-por-passo. Problemas da IMO recebem notas de 0-7, avaliados “de 7 para baixo” (próximos da completude) ou “de 0 para cima” (faltando ideia crítica); crédito parcial reflete progresso conceitual, não contagem de linhas [23][24]. O Putnam usa 0-10, mas efetivamente só concede as notas zero, um, dois, oito, nove e dez — o “Gap of Death” (3-7) é quase nunca usado, de modo que uma demonstração que carece de rigor total pontua ≤2 independentemente do trabalho circundante que pareça correto [12]. Isso sinaliza diretamente que crédito parcial julgado por humanos em demonstrações resiste a qualquer rubrica mecânica e aditiva — a mesma lacuna que avaliadores automatizados ainda não conseguem fechar (parte d).

(c) A taxonomia temática da matemática avançada e dos exames de qualificação de doutorado

A Mathematics Subject Classification (MSC 2020), mantida conjuntamente pela AMS/MathSciNet e zbMATH, é a coisa mais próxima de uma taxonomia oficial de toda a matemática: 63 códigos de nível superior de dois dígitos, de 00 General e 03 Logic até a família de álgebra (12-20), a família de análise/geomtria/topologia (26-58), probabilidade/estatística (60-62), áreas aplicadas (68 CS, 76-86 mecânica, 90-94 OR/teoria dos jogos/informação), até 97 Educação matemática [15][16]. Cada código subdivide-se em áreas de segundo nível com letras [15].

Os exames de qualificação de doutorado amostram um núcleo pequeno e bastante universal em vez das 63 áreas completas. Harvard nomeia seis: Álgebra (Sylow, anéis/módulos, Galois, teoria de representações), Geometria algébrica (variedades, Riemann-Roch), Análise complexa (teoria de Cauchy, resíduos, superfícies de Riemann), Topologia algébrica (grupo fundamental, (co)homologia, dualidade de Poincaré), Geometria diferencial (variedades, feixes, curvatura) e Análise real (teoria da medida, espaços Lp, análise de Fourier, EDPs, probabilidade, espaços de Sobolev) [13]. Outras instituições (TCU, UNT, Stanford, Penn State) exigem 2-4 exames de um menu semelhante, menor — confirmando que “nível de doutorado” significa profundidade em um punhado de pilares centrais, não cobertura enciclopédica da MSC [14].

(d) Formatos auto-avaliáveis para matemática avançada

STACK (Moodle, suportado pelo CAS Maxima) e WeBWorK (linguagem “PG” baseada em Perl) são os dois sistemas maduros e amplamente implantados para verificação de respostas numéricas/simbólicas: ambos validam a entrada, checam equivalência algébrica (não correspondência de string) via parâmetros aleatórios por estudante, e dão feedback instantâneo — nenhum deles afirma avaliar uma demonstração escrita [17][18][19]. A mesma técnica — subtrair, simplificar, checar se o residual é simbolicamente zero, ou recorrer à avaliação numérica — é o que bibliotecas ao estilo SymPy fornecem programaticamente, e sustenta os harnesses contemporâneos de avaliação de matemática por LLMs [25].

Para a avaliação de demonstrações propriamente ditas, a única abordagem mecanicamente sólida é um assistente de provas: Lean 4 + mathlib compila uma demonstração e a aceita ou rejeita — sem crédito parcial, mas sem ambiguidade [20]. O Natural Number Game (Imperial College London) demonstra que isso funciona como produto de ensino, gamificando os axiomas de Peano de modo que fatos “óbvios” como a+b=b+a precisam ser provados a um compilador; “Mathematics in Lean” estende a ideia ao conteúdo de graduação [20][21].

A avaliação de demonstrações em linguagem natural — o formato que os estudantes realmente escrevem — permanece sem solução. LeanTutor (2026) auto-formaliza um passo de demonstração em Lean, mas requer uma solução formalizada pré-existente [26]. IMO-GradingBench (2025), a partir de 1.000 soluções de IMO avaliadas por humanos, constatou que mesmo os modelos de ponta (o3, Gemini 2.5 Deep Think) alcançam apenas 52-54% de concordância exata com avaliadores humanos às cegas (sem referência), com erros concentrados em distinguir “parcial” de “errado”; humanos com referência correlacionam em 0,96 [22]. RefGrader (2025) melhora a confiabilidade ao sempre avaliar contra uma referência ao invés de às cegas, ao custo de precisar dessa referência pré-construída [27]. A avaliação de demonstrações em linguagem natural por IA é real, mas ainda pouco confiável nos limites mais difíceis para ser o único mecanismo de avaliação para feedback instantâneo e confiável.

Implicações de design para o Math Challenge

Bandas propostas acima do ensino médio, cada uma com tópicos concretos e — criticamente — um mecanismo honesto e realista de avaliação automática:

1. Band U1 — Transição para a Prova. Tópicos: lógica proposicional/predicativa, manipulação de quantificadores (ordem ∀/∃, negação), prova direta, contraprova, indução, prova por contradição, teoria básica de conjuntos e funções. Avaliação automática: múltipla-escolha/múltipla-seleção em “qual destas é a negação correta desta afirmação”, “insira o quantificador faltante”, e exercícios de ordenação de passos (embaralhar linhas de uma prova válida, o estudante as reordena) — isso atinge diretamente as falhas documentadas de quantificadores e estrutura encontradas por Selden & Selden e na literatura sobre ordem de quantificadores [3][5][6].

2. Band U2 — Validação de prova como habilidade própria. Apresentar uma “prova” curta com um defeito inserido (ordem de quantificador errada, passo não justificado, raciocínio circular) e pedir ao estudante que selecione a linha exata que quebra, ou classifique o argumento inteiro como válido/inválido/incompleto. Isso é motivado diretamente pela constatação de Selden & Selden de que a prática de construção não se transfere para a capacidade de validação — ela precisa de seu próprio tipo de exercício [3][4].

3. Band U3 — Álgebra Abstrata (grupos, anéis, corpos). Tópicos: axiomas de grupo, teorema de Lagrange, grupos cíclicos, homomorfismos/isomorfismos, grupos quocientes, teoria básica de anéis e corpos. Avaliação automática: respostas numéricas/estruturais (ordem de um elemento, este mapa é homomorfismo — sim/não com um elemento contra-exemplo requerido caso seja não), preenchimento de tabela de Cayley, múltipla-escolha em “qual axioma falha aqui”.

4. Band U4 — Análise Real. Tópicos: sequências/límites, continuidade ε-δ, diferenciabilidade, integração de Riemann, testes de convergência de séries. Avaliação automática: resposta numérica (encontrar N tal que |a_n − L| < ε), múltipla-escolha sobre qual teste de convergência se aplica, e entrada de contra-exemplo (“forneça uma sequência que converge pontualmente mas não uniformemente”) verificada contra uma biblioteca de contra-exemplos válidos mais um verificador simbólico/numerico (avaliar o candidato em pontos amostrais).

5. Band U5 — Álgebra Linear além do curso introdutório. Tópicos: autovalores/autovetores, diagonalização, forma de Jordan, espaços de produto interno, teorema espectral. Avaliação automática: totalmente numérica/simbólica — esta banda é essencialmente livre com um backend CAS equivalente ao SymPy (o modelo STACK/Maxima se aplica quase diretamente) [17][18].

6. Band U6 — Combinatória & Teoria dos Números (estilo olimpíada). Tópicos: princípio da caixa, invariantes, aritmética modular, funções geradoras, combinatória extremal — modelado diretamente na taxonomia de Engel e na estrutura AoPS/WOOT [8][10]. Avaliação automática: esta banda se encaixa melhor no modelo existente do Math Challenge — quase todos esses problemas têm uma resposta numérica única ou forma fechada final, exatamente como os problemas de preenchimento estilo AMC/AIME/Putnam, portanto não é necessário novo mecanismo de avaliação além do que a escada já oferece nas camadas inferiores.

7. Band G1 — Topologia. Tópicos: espaços métricos/topológicos, compacidade, conectividade, continuidade, fundamentos do grupo fundamental. Avaliação automática: múltipla-escolha (“este espaço é compacto — sim/não, escolha a cobertura que falha”), Verdadeiro/Falso com seleção de justificativa (escolher qual das 4 justificativas candidatas é a válida), já que provas topológicas abertas não são verificáveis mecanicamente sem formalização.

8. Band G2 — Teoria da Medida & Análise Real de Pós-graduação. Tópicos: σ-álgebras, medida de Lebesgue, funções mensuráveis, espaços L^p, convergência dominada. Avaliação automática: majoritariamente numérica (calcular uma integral de Lebesgue, determinar se uma função está em L^p) mais múltipla-escolha sobre qual teorema de convergência se aplica a um cenário dado — um mapeamento quase direto do programa de qualificação de análise real de Harvard [13].

9. Band G3 — Análise Complexa. Tópicos: holomorfia, teorema de Cauchy, resíduos, mapas conformes, teorema da aplicação de Riemann. Avaliação automática: numérica (avaliar uma integral de contorno via resíduos — tarefa clássica verificável por CAS) mais múltipla-escolha sobre classificação de singularidade.

10. Band G4 — Topologia Algébrica / Geometria Diferencial. Tópicos: cálculo de homologia/co-homologia para espaços padrão (esferas, toro, espaços projetivos), curvatura de superfícies padrão. Avaliação automática: numérica (números de Betti, característica de Euler) — computável e verificável — mas conteúdo de prova genuína (por exemplo, “prove a dualidade de Poincaré para este espaço”) não é autoavaliável e deve ser apresentado como conteúdo “exemplo trabalhado” somente leitura, não como desafio pontuado.

11. Band PhD-1 — EDPs & Probabilidade (núcleo de exame de qualificação). Tópicos: equações de calor/onda/Laplace, soluções fracas, fundamentos de imersão de Sobolev; probabilidade medida-teórica, funções características, teorema central do limite. Avaliação automática: verificação numérica de solução para EDPs canônicas (verificar se a solução candidata satisfaz a EDP e as condições de contorno via substituição direta — puramente mecânico e amigável a CAS) e questões de cálculo de probabilidade.

12. Band PhD-Lean — Trilha “Formalmente Verificada” de capstone, claramente rotulada como diferente das demais. Tópicos: sequência curada de pequenos lemas (no espírito do Natural Number Game) construindo um resultado não trivial, autorado em Lean 4 contra mathlib. Avaliação automática: o próprio compilador é o avaliador — uma prova recebe aprovação/reprovação mediante compilação bem-sucedida, sem ambiguidade de pontuação, ao custo de um investimento elevado de autoria (cada exercício precisa de um esqueleto verificável em Lean) e de uma curva de aprendizado real para o usuário (sintaxe Lean, não apenas matemática) [20][21].

13. Objetivo explícito não-alcancado: avaliação de provas em linguagem natural por IA, como mecanismo pontuado (não de feedback de tutor). Dado o acordo de ~52-54% de avaliação cega do IMO-GradingBench com juízes humanos mesmo de modelos de fronteira em 2025-2026 [22], o Math Challenge não deve lançar um recurso que atribua aprovação/reprovação ou pontuação numérica a provas escritas por estudantes via julgamento de LLM sozinho. É apropriado, porém, que o recurso existente “feedback de IA tutor após cada desafio” forneça comentários qualitativos, não pontuados, sobre um esboço de prova submetido (este é um recurso de coaching, não de avaliação pontuada, de modo que um julgamento errado ou excessivamente confiante é uma questão de qualidade UX, não de integridade de pontuação) — essa distinção (feedback vs. pontuação) é exatamente o que mantém as bandas de modo PhD honestas sobre o que “autoavaliável” significa.

14. Mecanismo transversal: adotar a ideia-chave do RefGrader — sempre avaliar contra uma referência, nunca às cegas — para qualquer julgamento assistido por IA usado em modo PhD. Como a avaliação baseada em referência supera mensuravelmente a avaliação cega [22][27], qualquer ponto em que o tutor avalie raciocínio aberto (não apenas o caso proibido acima) deve sempre receber a solução/rúbrica canônica como contexto, nunca ser solicitado a julgar uma prova sem referência.

Perguntas abertas para o dono do projeto

1. O “modo PhD” deve incluir a trilha de capstone verificada em Lean (item 12) dado seu custo de autoria, ou permanecer inteiramente em formatos numéricos/múltipla-escolha/contra-exemplo?
2. Uma revisão de esboço de prova por IA apenas como coaching (não pontuada) é aceitável para as bandas superiores, ou o produto precisa que todo desafio produza uma pontuação rígida de aprovação/reprovação?
3. As fronteiras das bandas devem seguir estritamente os códigos de nível superior da MSC (para um recurso “navegar por área MSC”) ou permanecer organizadas em torno do núcleo de exame de qualificação de PhD (que é mais estreito e pedagogicamente padrão)?
4. Existe demanda por licenciar/integrar um motor CAS existente (o pipeline Maxima do STACK é código-aberto e nativo do Moodle) ao invés de construir verificação numérica/simbólica do zero?