В репозитории OpenAI по математике обнаружены расхождения между заголовками статей и формализованными доказательствами в Lean

Анализ 242 заметок о диапазоне применения (scope notes) в репозитории OpenAI/math показал, что в десятках случаев заголовок результата не соответствует фактически проверенной формулировке в системе доказательств Lean. Это указывает на то, что формализация часто подтверждает лишь ослабленные или частичные утверждения, в то время как основные теоремы из оригинальных работ остаются за рамками проверенного кода.