dougdotcon/douvras-lean-proof-repair
Douvras Lean Proof Repair Corpus Exemplos sintéticos de erros comuns de reparo em Lean: importação ausente, incompatibilidade de tipos, falha de tática, meta não resolvida, reescrita inválida e prova reflexiva. Os snippets não foram executados no compilador (proof_status: NOT_EXECUTED); portanto o corpus não prova nenhum teorema e não substitui validação com uma versão específica do Mathlib.
Douvras Lean Proof Repair Corpus
Exemplos sintéticos de erros comuns de reparo em Lean: importação ausente, incompatibilidade de tipos, falha de tática, meta não resolvida, reescrita inválida e prova reflexiva. Os snippets não foram executados no compilador (proof_status: NOT_EXECUTED); portanto o corpus não prova nenhum teorema e não substitui validação com uma versão específica do Mathlib.