Como abater suas provas

59

Quais são as diretrizes gerais para verificar suas provas? Eu acredito que isso é importante para estudantes de pós-graduação como eu. Eu já sei o que precisamos fazer para provar algo, mas você sempre precisa verificar tudo antes de enviá-lo. Mesmo para o seu próprio consultor.

Desenvolvi algumas estratégias por tentativa e erro e recebi muitos conselhos do meu orientador. Mas este é sempre um trabalho muito tedioso. Normalmente, quando você termina algo, só quer continuar com o próximo problema, mas ainda precisa se ater ao problema atual até que tudo esteja perfeito. Aqui apresento um exemplo da minha própria lista de truques:

  1. Preencha os detalhes. Muitos erros existem em alguns lugares onde você escreve "é claro que ...", "sem perda de generalidade ...", etc.
  2. Experimente alguns números. Tente casos extremos, como "o que acontece quando eu defino ou ".n = 1000n=1n=1000
  3. Mantenha um notebook limpo. Escreva todos os dias nele e compare-o com suas anotações brutas. Tento escrever também em látex, encontrei muitos erros dessa maneira.

Quais são as estratégias gerais que você aplica para verificar suas provas?

O objetivo desta pergunta é torná-la um wiki da comunidade.

Marcos Villagra
fonte
Se a pergunta parecer subjetiva, ajude-me a melhorá-la.
Marcos Villagra
como faço para criar este wiki da comunidade?
Marcos Villagra
11
Ei, legal! Estou realmente interessado nas respostas a esta pergunta. Além disso, eu posso apreciar o seu # 3. (Quando penso sobre isso, na verdade tenho pilhas de papel espalhadas por toda parte quando estou trabalhando intensamente em um problema, que depois é realocado aleatoriamente. Eca.) Eu já cometi um erro antes dessa questão e acabei desperdiçando um bom pedaço de tempo.
Daniel Apon
@ Daniel: Eu tive o mesmo problema !! É por isso que, depois de terminar com uma prova, escrevo imediatamente a versão em látex. É bom saber que eu não sou o único cara confuso que mantém tudo em todos os lugares :-)
Marcos Villagra
11
você o sinaliza para atenção do moderador.
Suresh Venkat

Respostas:

39

Os engenheiros de software têm uma noção que chamam de " odores de código ". Esses são sintomas no código que podem indicar um problema mais profundo. Os engenheiros de software coletam listas mentais de odores para conhecer (ou seja, métodos excessivamente longos ou muitos parâmetros). Isso não significa necessariamente que há um problema, mas simplesmente indica que o escritor pode querer verificar novamente.

Proponho que devemos considerar também "cheiros à prova" . Isso não fornecerá um algoritmo para verificar suas provas, mas fornece uma linguagem e uma metáfora para o reconhecimento de possíveis problemas nas provas. Alguns exemplos de provas cheiram:

  1. Os advérbios "Claramente", "Obviamente", etc.
  2. Referência à prova de um resultado anterior em vez de uma referência ao resultado em si.
  3. Uso irreverente de um resultado com muitas pré-condições técnicas.

Há também cheiros mais sutis. Por exemplo, se uma prova usa o teorema do binômio para expandir uma expressão e depois usa o teorema do binômio para retornar a uma forma fechada, então talvez haja uma manipulação direta na forma fechada que dê o mesmo resultado.

Minha sugestão é coletar uma lista (mental ou escrita) desses odores e verificá-los enquanto você lê seu trabalho. O bom efeito colateral dessa abordagem é que ela também fará de você um melhor leitor.

Nota: Minha esperança nesta resposta era dar um lado intuitivo à resposta rigorosa fornecida por Como escrever uma prova de Lamport, mencionada na resposta de M. Alaggan.

Don Sheehy
fonte
4
Eu digo isso o tempo todo para meus alunos, e eles acham que eu sou louco. É claro que eu realmente afirmar que eu posso cheirar um erro, que pode ser parte do problema;)
Suresh Venkat
7
@Suresh: Este aluno pensa que você é louco por diferentes razões. ;-)
John Moeller 16/05
4
Na nota sobre o cheiro do código, as coisas que sempre tento examinar nas provas dos outros incluem cadeias de desigualdade. Muitas vezes, erros realmente básicos costumam aparecer entre as derivações mais difíceis.
John Moeller 16/05
23

Há um artigo muito bom de Leslie Lamport ( Como escrever uma prova ). Na verdade, é uma proposta dele sobre o estilo de escrever provas detalhadas de tal forma que:

(1) Permite detectar erros de maneira direta

(2) Torna claro quais suposições e teoremas são usados ​​em quais partes, o que facilita bastante ver o que acontece se você quiser (por exemplo) usar suposições mais fracas

Há também alguma experiência da comunidade e comentários inspiradores sobre esta técnica no MO, que mostram uma experiência positiva em geral (e alguns outros recursos também).

Atualização: existe uma nova versão Como escrever uma prova do século XXI .

M. Alaggan
fonte
5
Essas provas são muito semelhantes às que alguém escreveria em um trabalho de pesquisa em PL. A cadeia da lógica é muito explícita. Depois de aprender a ler e apreciar as provas no estilo PL, achei difícil entender as provas matemáticas "normais". Tais provas muitas vezes exigem que o leitor pense da mesma forma o autor faz, e quando você me acostumei com um estilo prova diferente, isso simplesmente não é o caso (para mim, pelo menos!)
Christopher Monsanto
2
@Christopher Monsanto: PL significa Linguagens de Programação? Eu apreciaria se você pode mencionar um exemplo tal (um tal papel) para verificar :)
M. Alaggan
5
Sempre tive a sensação de que o que Lamport sugere não é compatível com "A Mathematician's Lament" de Paul Lockhart ( maa.org/devlin/LockhartsLament.pdf ).
Marcos Villagra
14

Parece que me lembro de ter lido há muito tempo um relato popular de como os físicos lidam com um problema análogo. Quem sabe o quão precisa é a seguinte versão; correções são bem vindas. Mas achei a estratégia subjacente bastante notável.

Eles explicaram como chegaram a acreditar em buracos negros. Os buracos negros eram inicialmente construções puramente matemáticas, como outros objetos estranhos na física, como buracos de minhoca. A estratégia deles era impressionante: eles jogavam matematicamente outros objetos no objeto a ser testado. Buracos de minhoca falharam em seus testes porque descobriram que o buraco de minhoca entraria em colapso mesmo na presença de um objeto físico normal, talvez um asteróide. Mas os buracos negros passaram neste teste: o buraco negro sobreviveria com um asteróide jogado nele. Então eles tentaram jogar uma estrela nele. Mesmo resultado. Finalmente, eles jogaram outro buraco negro no buraco negro e ele sobreviveu. Como resultado disso, eles cresceram confiantes o suficiente na existência de buracos negros para realmente começar a procurá-los no universo real.

Portanto, a relevância e a aplicação da estratégia acima é começar a jogar as coisas à sua prova. Sobrevive às verificações de sanidade ? Se você remover uma suposição necessária, ela entra em colapso como deveria? Ele entra em colapso como deveria quando aplicado a casos fora de seu escopo? Suporta generalizações e especializações razoáveis? Dê uma olhada na lista de heurísticas em Como resolvê-lo . Tente alterar sua prova com essas heurísticas e veja se ela permanece e cai como deveria.

Pessoa tímida
fonte
A maior parte de sua resposta se concentra na verificação de provas, verificando se elas se tornam falsas em situações em que deveriam ser falsas. Isso não funciona porque não verifica se o teorema era verdadeiro onde deveria ser verdade! Por exemplo, suponha que eu "provei" que todo número ímpar é divisível por três. Verifico que minha prova falha se eu também estender para números pares: falha, pois quatro não é divisível por três. Viva, minha prova deve estar correta!
David Richerby
12

Eu acho que uma das abordagens mais seguras é apresentar várias provas independentes. Então você pode ter certeza de que seu resultado principal está correto, mesmo se você cometer algum erro em alguns detalhes de uma prova.

Jukka Suomela
fonte
9

Uma técnica que achei útil é pensar em quais outros resultados a estratégia de prova seria capaz de provar. Se eu sou capaz de adaptar facilmente a estratégia de prova para provar um grande problema em aberto ou mesmo um problema que não está aberto, mas que tem uma solução muito complicada em comparação com a complexidade da estratégia de prova, é um grande motivo para duvidar a prova.

Optar
fonte
5
PNP
6

Sempre reviso minhas provas com um verificador de provas como COQ ou ISABELLE . Se você pode provar sua prova em qualquer uma dessas linguagens de programação, pode ter certeza de que está correta. Tão simples quanto um termo lambda;).

Gopi
fonte
Eu nunca usei Coq, mas devo tentar. Na verdade, estou tentando provar alguns limites inferiores com o mathematica, mas não encontrei o caminho certo. Talvez eu precise de alguns pacotes especiais ou algo assim.
Marcos Villagra
11
Talvez seja uma possibilidade remota, mas se você quer provar alguns limites inferiores com reais, você pode verificar essas bibliotecas: coqtail.sourceforge.net/?home/en
Gopi
Concordou, mas qualquer linguagem de programação funciona. Na maioria das vezes eu faço isso ao contrário. Formule o domínio do problema em uma linguagem de programação (geralmente Ruby) e use-a como modelo para minha prova.
Chad Brewbaker