世界で最も難しい大学生数学コンテスト「パトナム」は昨日午後4時（太平洋標準時）に終了した。 午後 3 時 58 分までに、AxiomProver @axiommathai は、100% 検証可能な言語である Lean で Putnam2025 の 8/12 を自律的に解決しました。 昨年、私たちのスコアは約4000のうち4位で、パトナムフェロー（近年のトップ10）でした。
ウィリアム・ローウェル・パトナム試験は、世界で最も権威のある大学入試です。中央値は0点になることが多いです。 Axiomはパロアルトに拠点を置く設立4ヶ月のスタートアップです。私たちは推論の出発点、つまりAI数学者を構築しています。 Lean は 100% 機械検証可能な言語です。
これが私たちの第一歩です。 4ヶ月前、裏庭のセールでキャンピングカーの椅子とプラスチックのテーブルを購入しました。壁にはホワイトボードとポストイットが貼られていました。初めてのソファにみんな大喜びでした。 私たちは今、大西洋を越えて根を下ろしています。 数学とエンジニアリングの深い知識を持つチームが集結しました!
私たちの AxiomProver システムの背後にいる人々は、数学、プログラミング言語、AI という 3 つの柱を愛しています。 彼らは形式化が自然かどうかについて議論し、コンパイラ技術のおかげで証明が通ると興奮します。 この作品は技術的なものですが、人間的な側面も深く含んでいます。
私たちは、@leanprover、Mathlib コミュニティ、学術界と業界の研究者といった巨人たちの肩の上に立っています。 ありがとうございます。私たちは、今後のリリースを通じてコミュニティに貢献できるツールを開発しています。 私たちはパトナムの参加者に敬意を表し、皆さんの功績をすぐに祝福します。
@axiommathai はリツイートしていただけると嬉しいです!