(이 그림과 아래 내용은 내가 수학자도 아니고 논문을 다 이해할 수 있는 것도 아니라서 틀릴 수 있음)

정확히는 AI를 이용한 수학 연구를 위해 사용되는 Lean으로 번역하는 과정에 대해 반박이 들어온듯

컴퓨터의 성능이 점점 증가하면서 컴을 수학연구에 쓰려는 생각을 꽤 오래전부터 수학자들이 해왔음

그러다가 2013년에 마이크로소프트에서 개발한 수학 증명용 프로그래밍 언어인 Lean이 지금에는 광범위하게 보조용으로 쓰이고 있음

AI를 이용한 수학 연구 보조도 사실 자연어 논문을 그대로 주는게 아니라, Lean으로 번역해서 돌려보고 오류가 안뜨면 맞았다고 하는 식

이번에 open Ai는 나비에-스톡스 방정식을 증명했다고 주장하면서 자연어로 된 논문과 lean으로 된 코드를 같이 공개했음

그리고 몇백개의 증명과 오류가 안뜨는 lean 코드도 같이 공개함

근데 사실 자연어를 lean으로 번역하는 과정 자체가 디게 빡센 일인데

공개된 lean 코드를 보니 주장하는 내용과 딴소리를 하는 부분이 있는 것 같은데?라는 논문이 며칠 전 공개됨

이러면 엉뚱하거나 더 쉬운 내용을 증명해놓고 더 어려운 내용을 증명했다고 주장할수도 있는거임

좀더 파봐야겠지만 수학자들이 빡쳐하는 이유가 점점 더 이해되는듯