Parar problema vs.automatizada teorema de provar?

Question

Na Teoria da Computação tutorial oferecido pela Complexidade da Árvore (eu só começou o 2º vídeo), ele fala sobre como a suspensão problema foi desenvolvido para mostrar que a matemática não pode ser automatizada.Ultimamente, tenho ouvido falar bastante sobre os automática de teorema provando-algumas pessoas são mesmo postulado de que algum dia matemáticos serão substituídas por máquinas.A minha pergunta é:Precisamos encontrar uma falha no raciocínio de o Suster o problema de provar que a matemática pode ser automatizado?(Ou está a Travar o problema, na idade de Aprendizagem de Máquina, reduzida a um bom relato histórico do passado...)

Answer 1

A noção de automatizar a matemática é uma vaga, e que de contabilidade para a discrepância aqui.

Uma interpretação seria:para automatizar a matemática seria a de produzir uma máquina $M$ o que poderia dizer se é ou não uma frase é verdadeira (ou, mais fracamente, demonstrável a partir de alguns acordado conjunto de axiomas como $\mathsf{ZFC}$).Mesmo a versão mais fraca é descartada pelo incomputability de o suster o problema.

Outra interpretação é:para automatizar a matemática é a produção de uma máquina $M$ o que vai encontrar provas de todos os demonstrável (novamente, desde que acordado conjunto de axiomas) sentenças.Note que $M$ é não necessário para determinar se uma frase é demonstrável em primeiro lugar, apenas para encontrar uma prova se tal prova existe em todos os.Este é possível através de pesquisa de força bruta.

É claro que o segundo tipo de automação é altamente inviável - em geral, vai demorar ridiculamente tempo para encontrar provas de teoremas.Mas que não tem impacto sobre o seu princípio-possibilidade.Este é realmente o ponto de partida automatizado teorema de provar:trivialmente brute-force-prova-pesquisa é possível, e trivialmente é horrível em geral, podemos encontrar inteligente prova de estratégias de pesquisa em alguns casos de interesse?E é aí que a teoria da complexidade entra em cena.)

Answer 2

Você está comprimindo dois possíveis significados da frase "a matemática pode ser automatizado":

1. "qualquer teorema pode ser provada verdadeira ou falsa por um algoritmo"
2. "a atividade prática da prova de teoremas, como atualmente executadas por seres humanos, em vez disso, pode ser realizado por computadores de forma economicamente viável de moda"

Devido ao travar o problema, é impossível para qualquer algoritmo de ser capaz de provar ou refutar todos os teoremas.Mas isso se aplica tão bem para os seres humanos quanto para computadores!

Não há necessidade de ser uma falha na prova de a interrupção de um problema undecidability para (teoricamente) o trabalho humano matemáticos para se tornar obsoletos.Uma máquina não tem de ser capaz de resolver problemas indecidíveis para eliminar a função do humano matemáticos—ele só tem que ser capaz de provar teoremas de interesse de forma mais eficiente do que os seres humanos podem.Esta não é uma questão de computability ou assintótico complexidade computacional, mas de economia.

Não há nenhuma razão para pensar que os cérebros humanos são exclusivamente superior em provar teoremas matemáticos.Além disso, devido a Moravec paradoxo de, devemos esperar que os computadores poderiam ser melhores em provar teoremas que os seres humanos.O cérebro humano é um saco de carne, cuja história evolutiva inclui praticamente não fitness recompensas para o fenótipo de "pode revelar-se difícil teoremas." Assim, seria de esperar que a podemos ver um computador que está superintelligent na área de provar teoremas, mais cedo do que seria de esperar para ver um computador que está superintelligent na área de, digamos, de caça da megafauna.

Answer 3

Eu acho que esta pergunta deveria te dar o Resposta.

https:// cstheory.stackexchange.com / Perguntas / 2800 / If-P-NP-POTÁRIA-Obtenção de provas - de-goldbachs-conjeture-etc

Em suma, se p= np, qualquer conjectura com uma prova de comprimento razoável pode ser provada por um computador.