새 사전공개 논문이 AI가 수학 증명을 Lean으로 옮길 때 검증을 통과해도 원래 자연어 주장과 달라질 수 있다고 지적했다. 연구진은 OpenAI의 나비에 스토크스 관련 결과를 분석해 자연어에서 m+4차 미분 가능성을 쓰는 대목이 Lean에서는 m+5차 가정으로 강화되는 사례 등을 제시했다. 이는 원래 정리나 증명이 거짓이라는 단정이 아니라 서로 다른 명제를 검증할 위험에 대한 비판이다. OpenAI가 자연어 설명과 형식 증명을 함께 공개한 만큼, 두 버전의 가정과 결론이 일치하는지 살피는 검토가 중요해졌다.