Математики обнаружили расхождения в доказательствах OpenAI

Специалисты обнаружили несоответствия между текстовым доказательством OpenAI и его программной реализацией на языке Lean. Ошибки возникли при переводе математических рассуждений в код, что ставит под сомнение надежность автоматической проверки ИИ. В частности, условия в коде оказались менее строгими, чем в тексте, что меняет суть утверждения. OpenAI признала наличие расхождений, но подчеркнула, что это не делает само решение неверным. Компания планирует исправлять текстовые версии и продолжать работу над формализацией математики. Данный инцидент вызвал дискуссии о точности использования ИИ в точных науках.