Трактат о природе формального доказательства

[vsradkevich]

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

Все работает как скрипт в консольке!

[vsradkevich]

Может быть я и сошел с ума, но доказательства работают! Вся система полностью автономная!

Можно автоматически намайнить за ночь несколько диссертаций!

[vsradkevich]

Проверяю решения за сегодняшнюю ночь:

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

[vsradkevich]

Все формальные проверки по этой задаче успешно завершаются:

Коммиты сделаны, все изменения применены... 100% автоматически, можно повторять 1000 раз без ручного вмешательства, я проверял.

[vsradkevich]

Это лишь одно из сотен решений, найденных и проверенных