Lean4がテレンス・タオの最近の論文で小さなバグを見つけるのに貢献

• テレンス・タオのmathstodon.xyzへの投稿
• テレンス・タオの最近の論文で、Lean4形式化プロジェクトによって小さいが重要なバグが発見される
• 論文の6ページを形式化する過程でバグが見つかり、論文は https://arxiv.org/pdf/2310.05328.pdf で確認可能
• タオの論文で n=3, k=2 の場合に発散する式 12log⁡n−1n−k−1 が見つかる
• 問題は n の小さな値にのみ存在し、ページ内のいくつかの数値定数を変更することで解決可能
• n≥8 の場合は論理が依然として有効で、小さな n の場合はより簡単な方法で処理可能
• Lean4はタオに 0<n−3 を証明するよう求めたが、彼は n>2 という仮定しか持っておらず、矛盾が発生
• タオはLean4で形式化を試みた後に見つかった小さな誤りを認める脚注を、論文の新しいバージョンに追加する予定
• この投稿はコミュニティの関心と好意的な反応を呼び、将来の作業の堅牢な基盤を築くうえで証明支援ツールの重要性を強調

[GN⁺]

Hacker Newsのコメント

• 著名な数学者テレンス・タオが、Lean4とGPT-4を使って最近の論文にある小さなバグを見つけた。
• タオのLean4学習過程は彼のMastodon投稿に記録されており、Lean4がどのように作業を加速するかについての興味深いケーススタディになっている。
• 初心者には、Natural Number GameがLean4へのやさしい入門として勧められている。
• あるユーザーは、LamportのTLA+を使って形式仕様を作成し、プログラミングにおけるミスを減らした経験を共有した。
• コンパイラで実装する複雑さにもかかわらず、依存型に対する関心がある。
• Lean4と自動証明の組み合わせは、将来有望な技術的組み合わせに見え、新たな発見を促進する可能性がある。
• タオがCopilotを使ってLeanを学んでいることは、Lean4が新しいツールを採用する際の摩擦を減らせる方法の一例として強調された。
• タオのLean4に関する進捗は、彼のGitHubで確認できる。
• あるユーザーは、形式的証明チェッカーと言語モデルを組み合わせて合成的な予想-証明ペアを生成するというアイデアを提案しており、これは証明生成における超人的能力へと拡張できる可能性がある。
• 「バグ」という用語が数学的な誤りを説明するために使われており、一部のユーザーはそれを奇妙に感じていた.