Para lá do ensino secundário: demonstração, treino olímpico e matemática ao nível de doutoramento — o que o "modo PhD" poderia realmente conter

Constatações

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

A maioria dos departamentos dos EUA insere um curso de «transição para demonstração» entre o cálculo e o primeiro curso intensivo em demonstrações (álgebra, análise real) [1]. A sua pedagogia dominante é o método Moore: o docente fornece apenas axiomas e uma lista sequenciada de problemas; os estudantes não podem consultar textos, devem provar tudo eles próprios e apresentar uns aos outros [1][2]. A evidência de eficácia é sobretudo qualitativa e a longo prazo (mais estudantes a passar para a investigação) em vez de ser estritamente quantitativa [2].

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

O tratamento de quantificadores é a única área de falha mais replicada: um estudo com 61 estudantes constatou que nenhum conseguiu reescrever de forma consistente uma afirmação informal para o seu equivalente formal quantificado correto [1]. Modos de falha recorrentes: não introduzir uma variável ao provar uma afirmação universal; atribuir em excesso propriedades a um testemunho 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 a demonstração por contradição [5][6]. Um estudo de álgebra linear encontrou de forma semelhante estudantes a «falar um ao outro» sobre significados diferentes de «único» [6]. Estes são modos de falha discretos e bem definidos — cada um pode ser abordado por um exercício estreito e verificável (ver Implicações de Design).

(b) Como funciona o treino de olimpíadas

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

AoPS operacionaliza isto em escala — problemas antes das explicações, currículos desde Prealgebra até MATHCOUNTS/AMC/AIME/ARML e WOOT (treino de olimpíadas); todos os membros da equipa americana de IMO desde 2015 foram estudantes da AoPS [8]. A preparação para o Putnam segue o mesmo modelo orientado por conjuntos de problemas, reforçado por sessões de grupo em estilo de seminário [9][11].

A avaliação em ambos é deliberadamente grosseira e não‑aditiva — uma rejeição da pontuação por passo. Os problemas do IMO são avaliados de 0‑7, classificados ou «de 7 para baixo» (quase completo) ou «de 0 para cima» (faltando uma ideia crítica); o crédito parcial reflete o progresso conceptual, não a contagem de linhas [23][24]. O Putnam utiliza de 0‑10 mas, na prática, só atribui {0,1,2,8,9,10} — o «Gap of Death» (3‑7) é quase nunca usado, pelo que uma demonstração que carece de rigor total obtém ≤2 independentemente do trabalho circundante que pareça correto [12]. Isto é um sinal direto de que o crédito parcial avaliado por humanos em demonstrações resiste a qualquer rubrica aditiva e mecânica — a mesma lacuna que os 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 doutoramento

A Mathematics Subject Classification (MSC 2020), mantida em conjunto 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, desde 00 General e 03 Logic até à família de álgebra (12‑20), à família de análise/geomtría/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 identificadas por letras [15].

Os exames de qualificação de doutoramento amostram um pequeno núcleo bastante universal em vez das 63 áreas completas. Harvard enumera seis: Algebra (Sylow, anéis/módulos, Galois, teoria das 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, mas mais reduzido — confirmando que «nível de doutoramento» 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 implementados para a verificação de respostas numéricas/simbólicas: ambos validam a entrada, verificam a equivalência algébrica (não a correspondência de texto) através de parâmetros aleatórios por estudante, e fornecem feedback instantâneo — nenhum deles afirma avaliar uma demonstração escrita [17][18][19]. A mesma técnica — subtrair, simplificar, verificar se o residual é simbolicamente zero, ou recorrer à avaliação numérica — é o que as bibliotecas ao estilo SymPy fornecem programaticamente, e sustenta os harnesses contemporâneos de avaliação de LLMs de matemática [25].

Para a avaliação de demonstrações propriamente dita, a única abordagem mecanicamente sólida é um assistente de provas: Lean 4 + mathlib compila uma demonstração e aceita‑a ou rejeita‑a — sem crédito parcial, mas sem ambiguidade [20]. O Natural Number Game (Imperial College London) demonstra que isto funciona como produto de ensino, gamificando os axiomas de Peano de modo a que factos «óbvios» como a+b=b+a tenham de 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 — continua sem solução. LeanTutor (2026) auto‑formaliza uma demonstração passo a passo em Lean, mas necessita de uma solução de equipa já formalizada [26]. IMO‑GradingBench (2025), a partir de 1.000 soluções de IMO avaliadas por humanos, constatou que até os modelos de ponta (o3, Gemini 2.5 Deep Think) atingem apenas 52‑54 % de concordância exata com avaliadores humanos às cegas (sem referência), com erros concentrados na distinção entre «parcial» e «errado»; humanos com referência correlacionam‑se a 0,96 [22]. RefGrader (2025) melhora a fiabilidade ao avaliar sempre contra uma referência em vez 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 demasiado pouco fiável no limite mais difícil 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 secundário, cada uma com tópicos concretos e — crucialmente — um mecanismo de auto‑avaliação honesto e realista:

1. Band U1 — Transição para a demonstração. Tópicos: lógica proposicional/predicativa, manipulação de quantificadores (ordem ∀/∃, negação), demonstração direta, contrapositiva, indução, demonstração por contradição, teoria dos conjuntos básica e funções. Auto‑avaliação: escolha múltipla/multi‑seleção sobre «qual das seguintes é a negação correta desta afirmação», «insira o quantificador que falta», e exercícios de ordenação de passos (embaralhar as linhas de uma demonstração válida, o estudante reordena‑as) — isto dirige‑se diretamente às falhas documentadas de quantificadores e estrutura identificadas por Selden & Selden e na literatura sobre ordem de quantificadores [3][5][6].

2. Band U2 — Validação de demonstrações como competência própria. Apresentar uma curta «demonstração» 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 falha, ou classifique o argumento completo como válido/inválido/incompleto. Isto é motivado diretamente pela descoberta de Selden & Selden de que a prática de construção não se transfere para a capacidade de validação — requer o seu próprio tipo de exercício [3][4].

3. Band U3 — Álgebra abstrata (grupos, anéis, corpos). Tópicos: axiomas de grupos, teorema de Lagrange, grupos cíclicos, homomorfismos/isomorfismos, grupos quocientes, teoria básica de anéis/corpos. Auto‑avaliação: respostas numéricas/estruturais (ordem de um elemento, este mapa é um homomorfismo — sim/não com um elemento contra‑exemplo exigido se não), preenchimento de tabela de Cayley, escolha múltipla sobre «qual axioma falha aqui».

4. Band U4 — Análise real. Tópicos: sequências/limites, continuidade ε‑δ, diferenciabilidade, integração de Riemann, testes de convergência de séries. Auto‑avaliação: resposta numérica (encontrar N tal que |a_n - L| < ε), escolha múltipla 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 conhecidos válidos mais um verificador simbólico/número (avaliar o candidato em pontos amostrais).

5. Band U5 — Álgebra linear além do curso introdutório. Tópicos: valores próprios/vetores próprios, diagonalização, forma de Jordan, espaços com produto interno, teorema espectral. Auto‑avaliação: totalmente numérica/simbólica — esta banda é essencialmente livre com um motor CAS equivalente ao SymPy (o modelo STACK/Maxima aplica‑se quase diretamente) [17][18].

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

7. Band G1 — Topologia. Tópicos: espaços métricos/topológicos, compacidade, conectividade, continuidade, noções básicas de grupo fundamental. Auto‑avaliação: escolha múltipla («este espaço é compacto — sim/não, escolha a cobertura que falha»), Verdadeiro/Falso com seleção de justificação (escolher qual das 4 justificações candidatas é a válida), uma vez que demonstrações topológicas abertas não são verificáveis mecanicamente sem formalização.

8. Band G2 — Teoria da medida e 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. Auto‑avaliação: maioritariamente numérica (calcular uma integral de Lebesgue, determinar se uma função está em L^p) mais escolha múltipla sobre qual teorema de convergência se aplica a um determinado cenário — um mapeamento quase direto do programa de qualificação em análise real de Harvard [13].

9. Band G3 — Análise complexa. Tópicos: holomorfia, teorema de Cauchy, resíduos, mapas conformes, teorema de mapeamento de Riemann. Auto‑avaliação: numérica (avaliar uma integral de contorno via resíduos — uma tarefa clássica verificável por CAS) mais escolha múltipla sobre a classificação de singularidades.

10. Band G4 — Topologia algébrica / Geometria diferencial. Tópicos: cálculo de homologia/cohomologia para espaços padrão (esferas, toro, espaços projetivos), curvatura de superfícies padrão. Auto‑avaliação: numérica (números de Betti, característica de Euler) — computável e verificável — mas o conteúdo de demonstração genuína (por exemplo, «provar a dualidade de Poincaré para este espaço») não é auto‑avaliável e deve ser apresentado como conteúdo de «exemplo resolvido» apenas para leitura, não como um desafio pontuado.

11. Band PhD-1 — EDPs e Probabilidade (núcleo de exame de qualificação). Tópicos: equações de calor/onda/Laplace, soluções fracas, noções básicas de imersão de Sobolev; probabilidade medida‑teórica, funções característica, teorema do limite central. Auto‑avaliação: verificação numérica de soluções para EDPs canónicas (verificar se uma 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 — percurso de culminação «Formalmente Verificado», claramente rotulado como diferente do resto. Tópicos: uma sequência curada de pequenos lemas (no espírito do Natural Number Game) que conduzem a um resultado não trivial, criado em Lean 4 sobre mathlib. Auto‑avaliação: o próprio compilador é o avaliador — uma demonstração é avaliada como aprovada/rejeitada mediante compilação bem‑sucedida, sem ambiguidade de avaliação, ao custo de um investimento elevado na autoria (cada exercício requer um esqueleto verificável em Lean) e de uma curva de aprendizagem significativa para o utilizador (sintaxe Lean, não apenas matemática) [20][21].

13. Objetivo explícito não‑alcançado: avaliação automática de demonstrações em linguagem natural por IA, como mecanismo pontuado (não como feedback de tutor). Dado o acordo de ~52‑54 % de avaliação cega do IMO‑GradingBench com juízes humanos mesmo a partir de modelos de ponta em 2025‑2026 [22], o Math Challenge não deve disponibilizar uma funcionalidade que atribua um resultado de aprovado/rejeitado ou uma pontuação numérica a demonstrações escritas pelos estudantes através de julgamento apenas por LLM. É, porém, adequado que o já existente «feedback de tutor IA após cada desafio» forneça comentários qualitativos, sem pontuação, sobre um esboço de demonstração submetido (esta é uma funcionalidade de coaching, não uma avaliação pontuada, pelo que um julgamento errado ou excessivamente confiante é uma questão de qualidade UX, não de integridade de avaliação) — esta distinção (feedback vs. pontuação) é exatamente o que mantém as bandas em modo PhD acima honestas quanto ao que significa «auto‑avaliável».

14. Mecanismo transversal: adotar a ideia‑chave do RefGrader — avaliar sempre contra uma referência, nunca a cega — para qualquer julgamento assistido por IA usado em qualquer parte do modo PhD. Uma vez que a avaliação baseada em referência supera medivelmente a avaliação a cega [22][27], qualquer local onde 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 demonstração sem referência.

Questões abertas para o proprietário do projeto

1. Deve o «modo PhD» incluir o percurso de culminação verificado em Lean (item 12) dado o seu custo de autoria, ou permanecer inteiramente em formatos numéricos/escolha‑múltipla/contra‑exemplo?
2. É aceitável uma revisão de esboço de demonstração por IA apenas como coaching (não pontuada) para as bandas superiores, ou o produto precisa que cada desafio produza uma pontuação rígida de aprovado/rejeitado?
3. As fronteiras das bandas devem seguir estritamente os códigos de nível superior da MSC (para uma funcionalidade «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 interesse em licenciar/integrar um motor existente suportado por CAS (o pipeline Maxima do STACK é open‑source e nativo do Moodle) em vez de construir do zero a verificação de equivalência numérica/simbólica?