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

정확히는 AI를 이용한 수학 연구를 위해 사용되는 Lean 형식증명에 대한 내용인 듯

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

한 60년 정도 여러 시도가 있다가 2013년에 마이크로소프트에서 개발한

수학 증명용 프로그래밍 언어인 Lean이 지금에는 광범위하게 보조용으로 쓰이고 있음

AI를 이용한 수학 연구 보조도 사실 자연어 논문을 그대로 주는게 아니라,

자연어를 Lean으로 번역시킬 때 쓰거나, Lean으로 번역된 내용을 가지고 증명을 시도해보거나 하는거임 

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

근데 사실 자연어를 lean으로 번역하는 과정 자체가 문제의 내용을 통째로 바꿔버릴 수 있는 개빡센 일이라

이부분을 좀 파보니 공개된 lean 형식증명의 내용이 자연어 논문과 딴소리를 하는 부분이 있는거 같다는게 어제 공개된 내용임

문제-lean간의 번역 부분은 아직 확인중인 것 같은데 금방 파고드는 사람이 나올 듯함