Carina Hong(@CarinaLHong)의 스레드

Axiom의 퍼트넘 진술 공식화 작업은 정말 괴짜스러운 재미였습니다. 마치 증명하는 해커톤 같습니다. 증명하세요. 올해의 문제 공식화 품질을 보장하는 우리 팀에는 임페리얼 칼리지 런던, 케임브리지, MIT, 훔볼트의 대학원생이 포함되어 있습니다. 모두 Lean 커뮤니티에서 활발하게 활동하는 멤버이자 Zulip 사용자입니다. 많은 분들이 Mathlib 초기 기여자입니다. 일부는 대수기하학과 정수론 분야의 진지한 연구자입니다. 어떤 분들은 국가 올림피아드 대표팀 코치를 맡기도 하고, 어떤 분들은 (제가 포함시켜 달라고 요청한 부분입니다) 올림피아드 수학에서 특별히 좋은 성적을 거두지 못했습니다. 도전적인 수학 문제를 린 방식으로 바꾸는 것은 이상하게도 치료적일 수 있습니다. 수학을 위한 AI는 수학이 가져다줄 수 있는 놀라운 즐거움을 확장하고 있습니다. 서로 다른 경력 단계, 경쟁 수학과 다른 관계, 그리고 서로 다른 프로그래밍 경험을 가진 수학자들이 모여 문제를 프로그래밍 언어로 풀어내는 모습은 아름답습니다.