В математике существует несколько понятий, которые порой трудно понять, но значение слова “равно” казалось нам очевидным. Однако математики не могут прийти к единому мнению относительно того, что делает две вещи равными, и это вызывает проблемы у компьютерных программ, которые проверяют математические доказательства.
Эта дискуссия длится десятилетиями, но недавно достигла пика, поскольку компьютерные программы, используемые для формализации доказательств, требуют четких и конкретных инструкций. Двусмысленные определения математических понятий создают трудности для машин, которые не могут учитывать контекст.
Британский математик Кевин Баззард из Имперского колледжа Лондона столкнулся с этой проблемой при сотрудничестве с программистами. Это заставило его пересмотреть определения “равенства”, чтобы “оспорить различные разумные трактовки”. В своем препринте на сервере arXiv он пишет, что сначала думал, что понимает математическое равенство, но работа с компьютерными программами показала, что это понятие гораздо сложнее.
Знак равенства, впервые введенный валлийским математиком Робертом Рекордом в 1557 году, с тех пор эволюционировал. Современные математики используют его достаточно свободно, задавая уравнения и описывая различные математические объекты, представляющие одно и то же значение. Однако с конца 19 века, с развитием теории множеств, определение равенства стало еще шире.
Множество типа {1, 2, 3} может считаться равным множеству типа {a, b, c} благодаря каноническому изоморфизму, который сравнивает структуры групп. Однако принятие этого подхода вызывает сложности при формализации доказательств с использованием компьютеров. Баззард считает, что несоответствие между математическими и машинными представлениями равенства должно побудить ученых переосмыслить фундаментальные концепции, чтобы они стали понятны и для компьютеров.
