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

Все они – поклонники программы Lean. Это инструмент интерактивного доказательства теорем, который, в принципе, способен помогать математикам писать доказательства. Однако для этого математики должны вручную ввести математические правила в базу программы, приведя собранные за тысячи лет знания к виду, понятному компьютеру.

Для многих участников проекта его преимущества практически не требуют объяснений.

«На фундаментальном уровне очевидно, что после оцифровки чего-либо его можно использовать новыми способами, — сказал Кевин Баззард из Имперского колледжа Лондона. – И мы собираемся оцифровать математику, в результате чего она станет лучше».

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

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

Да и кто знает? Участвующие в проекте математики не всегда точно представляют себе, для чего может пригодиться цифровая математика.

«Мы не знаем точно, куда движемся», — сказал Себастиен Гёзель из Реннского университета.

Вы планируете, Lean работает

Летом группа опытных пользователей Lean проводила онлайн-семинар Lean для любопытных математиков. На первом занятии Скотт Моррисон из Сиднейского университета показал, как можно записать доказательство при помощи программы.