Que tipo de erro é um deslize trivial

Que tipo de erro é um deslize trivial

Pontos principais

1. Se um erro em alguma definição ou demonstração for fácil de corrigir, mas difícil de perceber, então esse erro não é trivial.
2. Alguns erros só podem ser encontrados com a ajuda de um assistente de provas.

Resumo do texto

• De dezembro do ano passado até 16 de abril deste ano, gastei cerca de 170 horas demonstrando o teorema de strings String.splitOn_of_valid na biblioteca padrão do assistente de provas Lean.
• Durante a demonstração desse teorema, encontrei um bug na definição da função String.splitOn.
• Corrigir esse bug não foi particularmente difícil. Bastou trocar i por i - j nessa definição.
• Ainda assim, não considero que esse erro tenha sido um deslize trivial. De acordo com essa definição, a função splitOn normalmente funciona corretamente, mas em casos especiais produz resultados incorretos.
• Se eu não estivesse usando um assistente de provas como o Lean, jamais teria encontrado um erro tão sutil.