Итак, реальности становится всё больше, она делается всё
разнообразнее. И даже что-то из неё снова хочется зафиксировать в
виде слов мало кому понятного языка. Странно, но ведь и правда людей,
понимающих русский язык, в процентном отношении не так уж и много.
Есть один такой голландец, Freek Wiedijk (он подсказывает, что это
читается как Phrake Weedike, и что никакой аналогии со словом "фрик"
его имя у соотечественников никогда не вызывает). Так вот, он, в
числе прочих безумных вещей, ведёт неофициальное соревнование между
различными proof assistant'ами вот здесь. Идея проста, как три рубля:
есть наугад выбранные сто "великих" теорем и нужно их
формализовывать. Кстати, интересно, как выглядит человек, который не
просто умеет сформулировать все эти сто теорем, но и их доказать.
Mizar, которым я заинтересовался ещё Бог весть когда, уже давно идёт
вторым с большим отставанием от лидера. Какое-то время назад (больше
года уже), я устремился немного помочь излюбленному proof assistant'у
и взялся формализовывать теорему Менелая и связанные с ней
результаты.
Теорема Менелая оказалась довольно элегантно обобщаемой в нескольких
направлениях. Можно обобщить её на случай многоугольника, на случай
угла в многомерном пространстве, либо обобщить немного вбок, и
связать её с отношениями площадей, а не просто с отношениями сторон.
К слову, в каком направлении обобщать эту теорему, я выяснял в
Ленинке, во время наших совместных туда походов с женой. И опять же,
к слову, это были одни из самых светлых моментов нашего в остальном
весьма безобразного брака.
Я формализовал обобщение на случай теоремы Рауса, исходя просто из
шести пересекающихся прямых на плоскости, не ограничиваясь
треугольником. И виде вся, елика сотвори. И се, добра зело:)
