형식 수학 라이브러리의 개발에 이바지하는 수학자가 많아질수록 성능이 좋은 수학 AI를 만들기가 수월해질 것입니다. 자신이 직접 린(Lean) 증명 보조기의 언어로 형식화한 수학 이론을 린의 수학 라이브러리 매스리브(Mathlib)에 옮기고 있는 한국인은 제가 알기로 현재 3명 있습니다.

저는 지난해에 매스리브를 린 3에서 린 4로 옮기는 작업에 조금 참여했고, 올해에는 린 4 배터리 라이브러리의 미해결 정리 하나를 증명했습니다.