来自 Carina Hong（@CarinaLHong）的推文线程

Axiom 对 Putnam 语句的形式化工作真是充满极客乐趣。这就像一场证明马拉松：证明大挑战。 负责确保今年问题形式化质量的团队成员包括来自伦敦帝国理工学院、剑桥大学、麻省理工学院和洪堡大学的研究生。 他们都是 Lean 社区的活跃成员和 Zulip 用户。许多人是 Mathlib 的早期贡献者。一些人是代数几何和数论领域的资深研究人员。一些人指导国家级奥林匹克竞赛队伍，还有一些人——这是他们要求我补充的——在奥林匹克数学竞赛中成绩并不理想。 将具有挑战性的数学问题转化为精益问题，可能会产生一种奇特的疗愈效果。 人工智能在数学领域的应用，正在拓展数学所能带来的无限乐趣。不同职业阶段、与数学竞赛有着不同渊源、拥有不同编程经验的数学家们齐聚一堂，将数学问题转化为编程语言，这本身就是一件美妙的事情。