Кофейный теоретик

Тут мне попалась на глаза (спасибо уважаемому Л.К.) лекция Теренса Тао про #AI

Там очень интересный обзор вполне конкретных применений компуктеров (не только ИИ) для решения мат. задач, начиная с пресловутой проблемы 4-х красок до наших дней.

Самый любопытный упомянутый сюжет это Lean. Про него есть коротко и есть длинно. Но если по сути, то эта штука умеет проверять математические рассуждения, если они записаны на некотором специальном языке (собственно на Lean).

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

Кстати, Тао отметил очень интересную штуку. Записанное в Lean доказательство становится интерактивным: то есть жмакнув по логическому переходу можно получить более подробно расписанный переход (о, как этого не хватает при виде всяких этих ваших "очевидно", "вычислением получаем", "легко видеть что" и прочего!). То есть доказательство, которое написано специалистом можно "раскрутить" до самых аксиом. Вот уж действительно, идеальный учебник.

Единственное, очень бы не хотелось, чтобы не заставили оформлять статьи по стандарту Lean. Вот это уж будет настоящая антиутопия 😊

Впрочем, я оптимист (про Тао не уверен, он об этом не особо говорил). Хотя ИИ сможет уже очень скоро (лет 10, запомните этот пост) эффективно проверять рассуждения, написанные нормальным языком (грубо говоря статью) и, возможно, проверять несложные гипотезы, но ИИ не сможет вести самостоятельных исследований. То есть едва ли он в обозримом будущем научится отличать полезные новые утверждения (хорошие теоремы) от бесполезных (плохие теоремы).

То есть он сможет написать статью для сборника РИНЦ "об одном асимптотическом свойстве одного решения одного уравнения", но на уровень не то что Тао, но даже и более скромных, но настоящих исследователей, — он вряд ли в обозримом будущем подымется. Впрочем, без "сборников РИНЦ" мы как-нибудь переживём.

Иначе говоря, я не сомневаюсь, что ИИ научится искать путь по дереву логических импликаций от аксиом к данному утверждению. Но я также не сомневаюсь, что в обозримом будущем ИИ сможет понять какие из всего многообразия следствий из аксиом (т.е. верных утверждений=теорем) — полезны, а какие не особо. Математика это вам не шахматы, тут критериев победы нету.

А вы как думаете, кожаные мешки с костями белковые исследователи?

Upd: спасибо Диме терешину, оригинал лекции.

YouTube

Гений Математики С IQ 230: Почему Будущее За ИИ

🧠💻🤖 Что происходит, когда человек с самым высоким IQ в мире (220-230) рассказывает о будущем математики? Теренс Тао, австралийский математический гений и обладатель престижнейших наград, включая премию короля Фейсала, шокирует своим откровенным взглядом на…

www.group-telegram.com/us/forodirchNEWS.com/2847

4.6K viewsedited  Nov 20 at 14:01

Тут мне попалась на глаза (спасибо уважаемому Л.К.) лекция Теренса Тао про #AI

Там очень интересный обзор вполне конкретных применений компуктеров (не только ИИ) для решения мат. задач, начиная с пресловутой проблемы 4-х красок до наших дней.

Самый любопытный упомянутый сюжет это Lean. Про него есть коротко и есть длинно. Но если по сути, то эта штука умеет проверять математические рассуждения, если они записаны на некотором специальном языке (собственно на Lean).

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

Кстати, Тао отметил очень интересную штуку. Записанное в Lean доказательство становится интерактивным: то есть жмакнув по логическому переходу можно получить более подробно расписанный переход (о, как этого не хватает при виде всяких этих ваших "очевидно", "вычислением получаем", "легко видеть что" и прочего!). То есть доказательство, которое написано специалистом можно "раскрутить" до самых аксиом. Вот уж действительно, идеальный учебник.

Единственное, очень бы не хотелось, чтобы не заставили оформлять статьи по стандарту Lean. Вот это уж будет настоящая антиутопия 😊

Впрочем, я оптимист (про Тао не уверен, он об этом не особо говорил). Хотя ИИ сможет уже очень скоро (лет 10, запомните этот пост) эффективно проверять рассуждения, написанные нормальным языком (грубо говоря статью) и, возможно, проверять несложные гипотезы, но ИИ не сможет вести самостоятельных исследований. То есть едва ли он в обозримом будущем научится отличать полезные новые утверждения (хорошие теоремы) от бесполезных (плохие теоремы).

То есть он сможет написать статью для сборника РИНЦ "об одном асимптотическом свойстве одного решения одного уравнения", но на уровень не то что Тао, но даже и более скромных, но настоящих исследователей, — он вряд ли в обозримом будущем подымется. Впрочем, без "сборников РИНЦ" мы как-нибудь переживём.

Иначе говоря, я не сомневаюсь, что ИИ научится искать путь по дереву логических импликаций от аксиом к данному утверждению. Но я также не сомневаюсь, что в обозримом будущем ИИ сможет понять какие из всего многообразия следствий из аксиом (т.е. верных утверждений=теорем) — полезны, а какие не особо. Математика это вам не шахматы, тут критериев победы нету.

А вы как думаете, кожаные мешки с костями белковые исследователи?

Upd: спасибо Диме терешину, оригинал лекции.

BY Кофейный теоретик