Parte VI · 1 — Matemática

draft

O domínio mais próximo do "superhumano" — porque a correção é verificável por computador, o que permite RL com recompensa perfeita.

🎨 Figura F-VI.1 — Prova verificada. Brief: um teorema sendo proposto por uma rede neural (nuvem) e checado por um verificador formal (engrenagem Lean) que acende um selo "✓ provado". Paleta do Compêndio.

Prova verificada

1.1 Por que matemática é especial

Provadores formais (Lean 4 / Coq / Rocq) verificam uma prova de forma exata. Isso dá uma recompensa perfeita para RLVR: gerou a prova → o verificador diz certo/errado → reward limpo. Sem ruído de rótulo humano.

1.2 Roadmap para equipe pequena

  1. Instalar Lean 4 + mathlib4.
  2. Base: DeepSeek-Prover-V1.5 ou Qwen2.5-Math-7B.
  3. SFT com mathlib + OpenMathInstruct + CoTs do DeepSeek-R1.
  4. RLVR: gerar prova candidata → checar no Lean → reward = passou/não-passou

    (GRPO).

  5. Test-time search: beam search + verificador formal.

Recursos realistas: 2–4 RTX 4090, 6–12 meses, 1 matemático consultor. É um dos projetos de "fronteira" mais acessíveis — ver alavancas em ../05-construindo-ia/01-alavancas-da-fronteira.kmd.

1.3 Marcos

AlphaGeometry e AlphaProof (2024) resolveram problemas de matemática olímpica combinando rede neural (intuição/proposição) + verificação formal — o paradigma neuro-simbólico (cap. 32).