Навье-Стокс потеряны при переводе: почему верификация в Lean не гарантирует корректность доказательств на естественном языке

Исследование показывает, что успешная формальная верификация в системе Lean не подтверждает корректность исходного доказательства на естественном языке, сгенерированного ИИ. Это выявляет критический разрыв между формальной логикой и семантикой человеческого языка в задачах автоматической формализации.