Как сбить ваши доказательства

59

Каковы общие рекомендации по проверке ваших доказательств? Я считаю, что это важно для аспирантов, как я. Я уже знаю, что нам нужно сделать, чтобы что-то доказать, но вам всегда нужно все проверять, прежде чем отправлять. Даже вашему собственному советнику.

Я разработал некоторые стратегии методом проб и ошибок и получил много советов от моего советника. Но это всегда очень утомительная работа. Обычно, когда вы заканчиваете с чем-то, вы просто хотите перейти к следующей проблеме, но вам все равно придется придерживаться текущей проблемы, пока все не станет идеально. Здесь я представляю пример моего собственного списка трюков:

  1. Заполните детали. Там было много ошибок, когда вы пишете «ясно, что ...», «без потери общности ...» и т. Д.
  2. Попробуйте несколько цифр. Попробуйте крайние случаи, такие как «что происходит, когда я устанавливаю или ».n = 1000n=1n=1000
  3. Держите чистую тетрадь. Пишите каждый день об этом и сравнивайте с вашими грубыми заметками. Я стараюсь писать и латексом, я нашел много ошибок таким образом.

Какие общие стратегии вы применяете для проверки своих доказательств?

Цель этого вопроса - сделать его вики-сообществом.

Marcos Villagra
источник
Если вопрос кажется субъективным, пожалуйста, помогите мне улучшить его.
Маркос Вильягра
как мне сделать это сообщество-вики?
Маркос Вильягра
1
Эй, круто! Мне действительно интересны ответы на этот вопрос. Также я могу оценить ваш # 3. (Когда я думаю об этом, у меня на самом деле повсюду разбросаны кучи бумаги, когда я напряженно работаю над проблемой, которая затем случайным образом перемещается. Фу.) Я уже столкнулся с ошибкой из-за этой самой проблемы и закончил тем, что тратил впустую хороший кусок времени.
Даниэль Апон
@Daniel: у меня была такая же проблема !! Вот почему после того, как я закончу с доказательством, я сразу же напишу латексную версию. Приятно осознавать, что я не единственный грязный парень, который хранит все везде :-)
Маркос Вильягра,
1
Вы отмечаете это для модераторского внимания.
Суреш Венкат

Ответы:

39

У разработчиков программного обеспечения есть понятие, которое они называют « запахами кода ». Это признаки в коде, которые могут указывать на более глубокую проблему. Инженеры-программисты собирают ментальные списки запахов, о которых нужно знать (т. Е. Чрезмерно длинные методы или слишком много параметров). Это не обязательно означает, что есть проблема, но просто указывает, что автор может захотеть перепроверить.

Я предлагаю также рассмотреть вопрос о «стойких запахах» . Это не даст вам алгоритм проверки ваших доказательств, но даст язык и метафору для распознавания возможных проблем в доказательствах. Некоторые примеры доказательств запахов:

  1. Наречия "Понятно", "Очевидно" и т. Д.
  2. Ссылка на доказательство предыдущего результата вместо ссылки на сам результат.
  3. Легкое использование результата со многими техническими предпосылками.

Есть и более тонкие запахи. Например, если в доказательстве используется биноминальная теорема для расширения выражения, а затем позже используется биноминальная теорема для возврата к закрытой форме, то, возможно, существует прямая манипуляция с закрытой формой, которая дает тот же результат.

Мое предложение состоит в том, чтобы собрать (мысленный или письменный) список таких запахов и проверить их во время чтения вашей работы. Приятным побочным эффектом этого подхода является то, что он также сделает вас лучшим читателем.

Примечание. В этом ответе я надеялся дать интуитивную сторону строгому ответу Лампорта «Как написать доказательство», указанному в ответе М. Алаггана.

Дон Шихи
источник
4
Я говорю это все время своим ученикам, и они думают, что я сумасшедший. Конечно, я на самом деле утверждаю, что чувствую запах жука, который может быть частью проблемы;)
Суреш Венкат
7
@ Суреш: Этот студент думает, что ты сумасшедший по разным причинам. ;-)
Джон Мёллер
4
В примечании к запаху кода вещи, которые я всегда стараюсь изучить в доказательствах других, включают цепочки неравенства. Часто по-настоящему базовые ошибки имеют обыкновение ползти среди более сложных выводов.
Джон Мёллер
23

Есть очень хорошая статья Лесли Лэмпорта ( Как написать доказательство ). Это на самом деле его предложение о стиле написания подробных доказательств таким образом, чтобы:

(1) Позволяет обнаруживать ошибки прямым способом

(2) Проясняет, какие предположения и теоремы используются в каких частях, что позволяет довольно легко увидеть, что происходит, если вы хотите (например) использовать более слабые предположения

Существует также некоторый опыт сообщества и вдохновляющие комментарии к этой технике на МО, которые показывают положительный опыт в целом (и некоторые другие ресурсы).

Обновление: появилась новая версия Как написать доказательство 21-го века .

М. Алагган
источник
5
Эти доказательства очень похожи на то, что можно было бы написать в исследовательской статье по PL. Цепочка логики очень четкая. После изучения того, как читать и оценивать доказательства в стиле PL, я обнаружил, что им трудно понять «нормальные» математические доказательства. Такие доказательства часто требуют, чтобы читатель думал так же, как и автор, и когда вы привыкли к другому стилю доказательства, это просто не тот случай (по крайней мере, для меня!)
Кристофер Монсанто
2
@ Кристофер Монсанто: PL означает Языки программирования? Я был бы признателен, если бы вы могли упомянуть такой пример (один такой документ), чтобы проверить :)
М. Алагган
5
У меня всегда было чувство, что то, что предлагает Лампорт, несовместимо с «Плачем математика» Пола Локхарта ( maa.org/devlin/LockhartsLament.pdf ).
Маркос Вильягра
14

Кажется, я помню, как давно читал популярный рассказ о том, как физики решают аналогичную проблему. Кто знает, насколько точна следующая версия; исправления приветствуются. Но я нашел основную стратегию довольно замечательной.

Они объяснили, как они поверили в черные дыры. Черные дыры изначально были чисто математическими конструкциями, как и другие странные объекты в физике, такие как червоточины. Их стратегия была поразительной: они математически бросали другие объекты в объект, который нужно проверить. Червоточины не прошли испытания, поскольку обнаружили, что червоточина разрушится даже в присутствии нормального физического объекта, возможно, астероида. Но черные дыры прошли это испытание: черная дыра выживет, если в нее будет брошен астероид. Поэтому они попытались бросить звезду в это. Тот же результат. Наконец, они бросили еще одну черную дыру в черную дыру, и она выжила. В результате они стали достаточно уверенными в существовании черных дыр, чтобы фактически начать искать их в реальной вселенной.

Таким образом, актуальность и применение вышеприведенной стратегии состоит в том, чтобы начать бросать вещи в свое доказательство. Выживает ли он в здравом уме ? Если вы удалите необходимое предположение, рухнет ли оно так, как должно? Разрушается ли он так, как должен, когда применяется к случаям, выходящим за рамки его действия? Выдерживает ли оно разумные обобщения и специализации? Взгляните на список эвристики в книге Поли « Как ее решить» . Попробуйте объединить свое доказательство с этими эвристиками и посмотрите, стоит ли оно и падает ли оно так, как должно.

Застенчивый человек
источник
Большая часть вашего ответа посвящена проверке доказательств, удостоверяющих, что они становятся ложными в ситуациях, когда они должны быть ложными. Это не работает, потому что это не проверяет, что теорема была верна там, где она должна была быть верной! Например, предположим, что я «доказал», что каждое нечетное число делится на три. Я проверяю, что мое доказательство не проходит, если я расширяю до четных чисел: да, так как четыре не делится на три. Ура, мои доказательства должны быть верными!
Дэвид Ричерби
12

Я думаю, что один из самых безопасных подходов - это предложить несколько независимых доказательств. Тогда вы можете быть уверены, что ваш основной результат верен, даже если у вас есть ошибка в некоторых деталях доказательства.

Юкка Суомела
источник
9

Один метод, который я нашел полезным, - это подумать о том, какие другие результаты сможет доказать стратегия доказательства. Если я легко смогу адаптировать стратегию доказательства, чтобы доказать большую открытую проблему или даже проблему, которая не открыта, но которая имеет слишком сложное решение по сравнению со сложностью стратегии доказательства, то это большая причина сомневаться доказательство.

выбирать
источник
5
Я бы дал +10, если бы мог - особенно в теории сложности, часто можно показать ошибочные методы доказательства, доказывающие действительно сильные утверждения, такие как , и тогда очень легко догадаться, что ваш метод доказательства неверен. Особенно, если ваша техника доказательства релятивизируется! PNP
Джошуа Грохоу
6

Я всегда перепроверяю свои доказательства с помощью средства проверки, такого как COQ или ISABELLE . Если вы можете доказать свое доказательство на любом из этих языков программирования, вы можете быть уверены, что ваше доказательство является правильным. Так же просто, как лямбда-термин;).

Гопи
источник
Я никогда не использовал Coq, но я должен попробовать. На самом деле, я пытаюсь доказать некоторые нижние границы с Mathematica, но я не нашел правильный путь. Может быть, мне нужны специальные пакеты или что-то в этом роде.
Маркос Вильягра
1
Может быть, это длинный пример, но если вы хотите доказать некоторые нижние границы с реалами, вы можете проверить эти библиотеки: coqtail.sourceforge.net/?home/en
Gopi
Договорились, но любой язык программирования работает. Чаще всего я делаю это наоборот. Сформулируйте проблемную область на языке программирования (обычно Ruby), а затем используйте это в качестве шаблона для моего доказательства.
Чад Brewbaker