アリストテレスによる@HarmonicMathによる自動形式化と、GPT Codex CLI(実際にはGPT-5.2でxhighとすべての実験的特典を有効にしたもの)でリバースエンジニアリング@OpenAI。Bourbakiの代数の行列に関する演習問題を扱い、証明の詳細を含むほぼ900行の完全に文書化されたLean 4コードを取得しました。 その後、適切に設計されたエージェント設定を使ってCodex CLIに渡し、対応するLaTeXファイルをリバースエンジニアリングし、Leslie Lamportの構造化証明スタイルでLeanから証明ステップを再構築しました。 まだラングランズ計画ではありませんが、この種の中級レベルの数学を自動化する必要があります。そして今まさにそれが起きています。適切なエージェント設定を構築し、すべてパイプライン化し、Bourbakiからテキストをスクレイピングしました(その部分も@grok 4.1でうまく動作し、LaTeXのライブプレビューには便利です)。 ドキュメントを完成させてGitHubに投稿します。依存グラフを確認してください。アリストテレスはそれを単独で処理しました。そして証明は完全にインタラクティブです。 私たちは今、科学の未来に生きています!

このコミュニティ投稿では、プログラミングと数学の両方で高度な概念を探求するのに役立つ、非常に魅力的なゲームやインタラクティブな環境(無料で入手可能)へのリンクを載せたいと思います。他に楽しい場所をご存知でしたら、ぜひ下に投稿してください。楽しんでください！ リーン: 数学がどのように証明され、形式化されるかを学ぶのに役立つ、非常に魅力的なプログラミングパズルのコレクションです。5*7=7*5の硬さを同じように見ることはもう二度とありません。 NandGame: 自分で一からプロセッサを作ればいいのです(NANDもよりシンプルな回路で作られています)。とても中毒性があり、とても楽しいです! クアンタム・フライトラップ: ここでようやく量子計算の理解が得られます。カラフルで無限、魅力的で、数学的に非常に深みがあります。 スクラッチ: 楽しい方法でプログラミングを学びましょう。 ユークリデア: 定規とコンパスでの作り方を学びましょう。以前は学校の教育の一部でしたが、今はアプリになっています。楽しくてとても有益でした。 平面性: それが確かに平面であることを示すグラフ埋め込みを探してみてください。 おおっと: 究極のセルラーオートマトン探検家。 もっと深く知りたいなら: セージマス: これはPython構文を用いた強力なコンピュータ代数システムです。コースに理想的で、SageMathの構文は一般的な数学的議論にずっと近いです。私はSageMathで授業を教えるのが好きです。 GeoGebra: 証明や計算、インターナティブアプレットなどもできます。これは未卒業数学のさまざまな側面を学ぶ楽しい方法です。 ウルフラムのデモンストレーションプロジェクト: 非常に高度なトピックを理解するのに役立つ数学アプレットのコレクションです。Mathematicaは動作させるのに必要ありませんが、自分でアプレットを設計するには必要です。 『証明の仕組み』(ヘザー・マクベス著): これはインタラクティブなGitHubリポジトリ付きの本で、Leanの構造や構文をより包括的に学べます。 『An Illustrated Theory of Numbers』(マーティン・H・ワイスマン著): これは初等数論とその応用に関する教科書です。これらのアプリケーションは、ウェブサイトから無料のJupyterノートブックのコレクションとして提供されており、重要な概念を教えてくれます。 グラフィカル線形代数: 代数の深い概念を学ぶための図解付き、ある程度インタラクティブな方法で学びます。 HomotopyContinuation.jl: これは、代数幾何学(連結成分、ホモトピー継続法)から非常に複雑な概念を学ぶ非常に美しくインタラクティブな方法です(ジュリアと共に)。また、応用から得られる非常に特殊な代数系への応用も可能です。その途中でジュリアを学べるよ。 Mathamaze: これはヘレナ・ヴェリルによる体験です。美しい幾何学、タイル、パターン。本当に素晴らしいです。 説明が難しいです: N:忍者の道: 数学が難しいと思うなら。忍耐は身をもって学びましょう。警告:非常に依存性が高い ハイパーローグ: ローグライク環境で双曲幾何学を学べます。

ここでは、最近の数学のレポートを完全に自己定式化したものを(またしても!)紹介します。 バランチュク、ステファン。「有限体上のn空間の部分集合を定義する方程式の数を減らす」トゥールーズ科学部年報:Mathématiques、シリーズ6、第33巻、第1号(2024年):177–182。 このプロジェクトに数日かけました。まず、アリストテレスを@HarmonicMathで解析し、約15時間で証明を完全に自動形式化しました。そして、@PietroMonticoneの大きな助けを借りて、証明の設計図版を作成することができました。このバージョンでは、LaTeXのすべてのドキュメントがインタラクティブになり、検査や学習が可能です。証明の依存関係を見て、それらの関係を研究することができます。 後処理段階では、Grok HeavyとCodex CLIを使い、xhighモードのGPT-5.2を使って形式証明の行ごとの分析を書きました。これは、プロのLean 4プログラマーでない人にとって非常に役立ちます。証明のすべてのステップを本当に内面化できます。 この経験から得た印象と学んだことをまとめたいと思います。@vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei