Доказательство в коде: как машина истины меняет математику и искусственный интеллект на русском

«Самая интересная книга о математике, которую я когда-либо читал». — Кевин Руз, обозреватель New York Times по вопросам технологий и соведущий подкаста Hard Fork.

Книга «Доказательство в коде» рассказывает внутреннюю историю Lean, компьютерной программы, которая отвечает на извечный вопрос: как узнать, истинно ли что-либо?

Всё началось с малоизвестной программы проверки ошибок в исследовательском центре Microsoft, разработанной одиноким инженером-программистом Лео де Моурой. Затем о ней узнала необычная группа математических чудаков, которые с мессианским рвением взялись за её внедрение. Их целью было создание машины истины, способной обеспечить самую редкую вещь в жизни: полную, стопроцентную гарантию истинности чего-либо. Её название: Lean.

По мере роста движения и укрепления возможностей программы к ней присоединились два самых выдающихся математика мира: Питер Шольце и Теренс Тао. Google DeepMind, Meta AI и другие технологические компании начали использовать программу для значительного повышения эффективности компьютерного мышления. Теперь она переосмысливает многотысячелетнюю историю того, как математики работают, сотрудничают и оценивают истину, прокладывая новый путь на пути к машинному интеллекту.

В книге «Доказательство в коде» Кевин Хартнетт рассказывает исчерпывающую историю зарождения и становления концепции бережливого производства (Lean) и о том, как это растущее движение трансформирует математику и открывает новую эру сотрудничества человека и компьютера. Увлекательное, основанное на характерах персонажей повествование, наполненное глубокими размышлениями о будущем математики, компьютеров и искусственного интеллекта, эта блестящая журналистская работа от одного из ведущих мировых авторов, пишущих о математике, предлагает глубокий ответ на вопрос: могут ли компьютеры раскрыть универсальные истины?