來自 Carina Hong（@CarinaLHong）的推文串

Axiom 對 Putnam 語句的形式化工作真是充滿極客樂趣。這就像一場證明馬拉松：證明大挑戰。 負責確保今年問題形式化品質的團隊成員包括來自倫敦帝國學院、劍橋大學、麻省理工學院和洪堡大學的研究生。 他們都是 Lean 社群的活躍成員和 Zulip 用戶。許多人是 Mathlib 的早期貢獻者。有些人是代數幾何和數論領域的資深研究人員。有些人指導國家級奧林匹克競賽隊伍，還有一些人——這是他們要求我補充的——在奧林匹克數學競賽中成績並不理想。 將具有挑戰性的數學問題轉化為精實問題，可能會產生奇特的療癒效果。 人工智慧在數學領域的應用，正在拓展數學所能帶來的無限樂趣。不同職業階段、與數學競賽有著不同淵源、擁有不同程式設計經驗的數學家們齊聚一堂，將數學問題轉化為程式語言，這本身就是一件美妙的事情。