딥마인드에서 만든 PS 문제푸는 AI가 코드포스에서 인간 상대로 상위 54% 성적을 냈다고 함





https://openai.com/blog/formal-math/


고등학교 수학 올림피아드 수준 문제를 푸는 벤치마크 MiniF2F에서 42.1%를 달성했다는데 정확히 어떤 의미인지는 모르겠고

Lean이라는 증명언어?로 표현해서 푸는건갑네



아직 자세히 안읽어봤는데 누가 읽고 요약 '해줘'