Carina Hong（@CarinaLHong）のスレッド

Axiom による Putnam ステートメントの形式化の取り組みは、まさにオタク的な面白さでした。まるで証明ハッカソンの Prove-a-ton のようです。 今年の問題の形式化の品質を保証する私たちのチームには、インペリアル・カレッジ・ロンドン、ケンブリッジ、MIT、フンボルトの大学院生が含まれています。 全員がLeanコミュニティのアクティブなメンバーであり、Zulipユーザーです。多くはMathlibの初期貢献者です。中には代数幾何学や数論の真摯な研究者もいます。オリンピック代表チームのコーチもいますし、オリンピックの数学がそれほど得意ではなかった人も（これは彼らから私に書いてほしい部分です）。 難しい数学の問題をリーンに変えることは、奇妙なほど治療効果があることがあります。 数学のためのAIは、数学がもたらす計り知れない喜びを広げています。キャリアステージ、競技数学との関わり、プログラミング経験の異なる数学者たちが、力を合わせ、問題をプログラミング言語へと変換していく過程には、素晴らしいものがあります。