ChatGPT 5, continued

 Продолжаю играть и работать с сабжем. Дал ей доказать некое алгебраическое утверждение, которое в принципе можно доказать прямым вычислением, но я не знаю как, потому что вычисление трудное и запутанное. Специальный случай word problem. То есть, нахрапом не возьмешь, соображать надо. Машинка меня удивила, выдав правдоподобное доказательство, основанное на геометрической интуиции. Я попросил формализовать его на языке LEAN (самый популярный proof verification assistant). Но тут коса нашла на камень. Код, выданный машинкой, содержал громадное количество ошибок. Потратил целый день на то, чтобы машинка их исправила. Некоторое время мы с ней ходили по кругу, я чуть не махнул рукой. В конце концов, все ошибки были исправлены, но теорема все равно не была доказана, потому что получился timeout. То есть LEAN как то умудрился превысить максимально возможное число итераций в процессе упрощения каких то выражений. Обидно.

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