Как стать автором
Обновить

Комментарии 3

Для интересующихся вопросом рекомендую недавнее исследование «Начал» Евклида. Авторы попытались максимально строго воспроизвести утверждения и доказательства из первой книги «Начал» и проверить их с помощью автоматизированных систем проверки доказательств (Coq, HOL Light).

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

Гильберт был в общем-то прав относительно евклидовой геометрии: ее можно формализовать, обходясь без картинок. Но в поиске решения геометрических задач картинки служит важным подспорьем и источником вдохновения. Можете в этом убедиться, попробовав вписать квадрат в окружность с помощью ровно 7 прямых или окружностей: Задача 1.7 в Euclidea. Это и так сложная головоломка, а без картинки ее практически нереально решить.
Судя по последней иллюстрации, ещё древние египтяне обладали привычкой выкидывать конспекты, как только сдан экзамен :)
Похоже статья была написала чтобы убедить грантодаталей в том что деньги были потрачены не зря, мол кривые чертежи откроют дорогу к будущему т.к. они ключ к прошлому и т.п.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий

Публикации