非専門的シンギュラリティー研究所

無限に動き続けるシステムを表す方法を AI なども使って考えていきます。

数学ゲーム(22)

中国の剰余定理パズル(9)

ChatGPT でアイコンの作り方を教えてもらいました。一つの画像のアイコンはできましたが複数の画像を持つアイコンの作り方はまだわかりません。今回は一つの画像のアイコンを使うことにしました。

アイコンは以下のようにしました。「ユークリッドの互除法」のように変数を置き換えて繰り返すイメージを  y = x^3 y = x^{12} のグラフを組み合わせて表したものです。

「中国の剰余定理パズル」のアイコン

準備ができたら公開する予定です。

以下は ChatGPT で調べた内容です。

Windows のアイコンの作り方を教えてください

と入力すると以下のような結果になりました。

Windows のアイコン(`.ico` ファイル)は、複数サイズの画像をまとめた形式です。
アプリケーション、ショートカット、フォルダーなどに使われます。

Windows アイコンの基本

Windows のアイコンには通常、複数の解像度が含まれます。

よく使われるサイズ:

  • 16×16
  • 24×24
  • 32×32
  • 48×48
  • 64×64
  • 128×128
  • 256×256

最近の Windows では 256×256 PNG 圧縮入り ICO がよく使われます。



方法1: 画像から `.ico` を作る(簡単)

手順

1. 元画像を作る

PNG 形式がおすすめです。

  • 背景透明にできる
  • 高画質
  • 編集しやすい

おすすめサイズ:

  • 256×256
  • 512×512



2. ICO に変換する

変換サイトやソフトを使います。

例:

PNG を読み込んで `.ico` で保存します。



方法2: GIMP で作る

画像編集ソフトの GIMP (https://www.gimp.org/?utm_source=chatgpt.com) を使う方法です。

手順

1. 新規画像作成
2. 透明背景にする
3. 絵を描く
4. 「ファイル」→「名前を付けてエクスポート」
5. `icon.ico` と入力
6. ICO 形式で保存

保存時に複数サイズを指定できます。



方法3: Visual Studio のアイコンエディタ

Visual Studio (https://visualstudio.microsoft.com/ja/?utm_source=chatgpt.com) にはアイコン編集機能があります。

手順

1. プロジェクトを開く
2. 「追加」→「新しい項目」
3. 「アイコンファイル」を選択
4. ドット単位で編集

Windows アプリ開発では便利です。



C# アプリにアイコンを設定する方法

WinForms / WPF

Visual Studio

1. プロジェクト右クリック
2. 「プロパティ」
3. 「アプリケーション」
4. 「アイコンとマニフェスト」
5. `.ico` を選択

EXE のアイコンになります。



C# でアイコンを読み込む

this.Icon = new Icon("icon.ico");

フォームのアイコンを変更できます。



アイコン作成のコツ

小さいサイズでも見やすくする

16×16 では細かい絵は潰れます。

良い例:

  • 太い線
  • シンプルな形
  • 強いコントラスト



背景透明を使う

透明背景 PNG → ICO にすると綺麗です。



複数サイズを入れる

Windows は状況によって自動選択します。



プログラムで ICO を作る

C# でも作れますが、ICO 形式は少し複雑です。

簡単には:

1. `Bitmap`
2. PNG 保存
3. ICO 変換ライブラリ使用

を行います。



アイコンデザイン例

よくある Windows アイコン:

  • フォルダー
  • 歯車
  • ターミナル
  • メモ帳
  • 数学記号
  • ツリー構造
  • 回路図

ユーザーの「構文木編集」「証明ゲーム」系のソフトなら、例えば:

  • 木構造アイコン
  • λ 記号
  • 数式ノード
  • パズルピース
  • グラフ構造

などが合いやすいです。



AI でアイコン画像を作る

最近は生成AIで:

  • ドット絵風
  • Windows 95風
  • フラットデザイン
  • 3D風

などのアイコン画像を作ってから ICO 化することも多いです。

プログラムで描画した画像を使いたいのでさらに質問してみました。

C# で ICO を作る方法を教えてください

と入力すると以下のような結果になりました。

C# で `.ico` ファイルを作るには、主に次の方法があります。

1. `Bitmap` を作る
2. ICO 形式で保存する

ただし、`.ico` は BMP や PNG より構造が複雑なので、
「バイナリを書き込む」か「ライブラリを使う」方法になります。



最も簡単な方法

PNG を作って ICO に変換

実用上はこれが簡単です。

using System.Drawing;

class Program
{
    static void Main()
    {
        Bitmap bmp = new Bitmap(256, 256);

        using (Graphics g = Graphics.FromImage(bmp))
        {
            g.Clear(Color.Transparent);

            g.FillEllipse(Brushes.Blue, 32, 32, 192, 192);

            g.DrawString(
                "C#",
                new Font("Arial", 48),
                Brushes.White,
                60,
                80);
        }

        bmp.Save("icon.png");
    }
}

これで PNG を生成できます。

その後 ICO 変換します。



C# だけで ICO を保存する方法

Windows ICO の最低限の構造を書き込みます。

以下は「1枚の32x32アイコン」を保存する簡易版です。

using System;
using System.Drawing;
using System.Drawing.Imaging;
using System.IO;

class Program
{
    static void Main()
    {
        Bitmap bmp = new Bitmap(32, 32);

        using (Graphics g = Graphics.FromImage(bmp))
        {
            g.Clear(Color.Transparent);

            g.FillRectangle(Brushes.Red, 0, 0, 32, 32);

            g.DrawEllipse(Pens.White, 4, 4, 24, 24);
        }

        SaveAsIcon(bmp, "icon.ico");
    }

    static void SaveAsIcon(Bitmap bmp, string path)
    {
        using (MemoryStream pngStream = new MemoryStream())
        {
            bmp.Save(pngStream, ImageFormat.Png);

            byte[] pngBytes = pngStream.ToArray();

            using (BinaryWriter writer =
                   new BinaryWriter(File.Open(path, FileMode.Create)))
            {
                // ICONDIR
                writer.Write((short)0);     // reserved
                writer.Write((short)1);     // image type
                writer.Write((short)1);     // number of images

                // ICONDIR entry
                writer.Write((byte)bmp.Width);
                writer.Write((byte)bmp.Height);
                writer.Write((byte)0);      // color count
                writer.Write((byte)0);      // reserved

                writer.Write((short)1);     // color planes
                writer.Write((short)32);    // bits per pixel

                writer.Write(pngBytes.Length);

                writer.Write(6 + 16);       // offset

                // image data
                writer.Write(pngBytes);
            }
        }
    }
}

これで `icon.ico` が生成されます。



ICO ファイル構造

ICO は:

  • ヘッダー
  • エントリ一覧
  • 画像データ

から構成されます。

ICONDIR

2 bytes  reserved
2 bytes  type
2 bytes  image count



ICONDIRENTRY

1 byte   width
1 byte   height
1 byte   color count
1 byte   reserved
2 bytes  planes
2 bytes  bit count
4 bytes  image size
4 bytes  offset



複数サイズを含む ICO

Windows アイコンは普通:

  • 16x16
  • 32x32
  • 48x48
  • 256x256

などをまとめて入れます。

C# で作るなら:

List<Bitmap>

を順番に ICO に書き込みます。



Windows Forms でアイコンを作る例

構文木エディタのようなアプリなら:

g.DrawRectangle(...)
g.DrawLine(...)

で:

  • 木構造
  • ノード
  • 数式
  • グラフ

などを描いて ICO にできます。



ドット絵風アイコン

16x16 のアイコンはドット絵感覚で作ると綺麗です。

bmp.SetPixel(x, y, Color.Black);

で1ピクセル単位で描画できます。



高品質アイコンを作るコツ

256x256 を含める

最近の Windows は高DPIなので重要です。



PNG 圧縮を使う

Vista 以降の ICO は PNG を内部に入れられます。

上のコードは PNG 内包型です。



小サイズ用に別デザインを作る

16x16 用は:

  • 文字を減らす
  • 太線にする
  • 単純化する

と見やすくなります。



さらに高度なこと

C# では:

  • EXE からアイコン抽出
  • DLL のアイコン取得
  • Shell アイコン取得
  • ファイル関連付けアイコン生成

などもできます。

例えば:

Icon.ExtractAssociatedIcon(path)

で EXE のアイコン取得ができます。

数学ゲーム(21)

中国の剰余定理パズル(8)

いろいろ書き直して動くようになりました。アイコンを設定しようと思ったのですが、まだやり方がよくわかっていません。アイコンができれば公開する予定です。

パズルの説明

  •  m n を互いに素な自然数、
  •  a 0 \le a \lt m である自然数、
  •  b 0 \le b \lt n である自然数

とするとき、

  •  m で割ると  a 余り、
  •  n で割ると  b 余る

 0 以上  mn 未満の数を求めるプログラムを完成させるパズルです。「中国の剰余定理」によりこのような数がただ一つ存在します。

起動すると以下の画面が表示されます。

中国の剰余定理パズル
(1) コード領域(最大公約数を求める関数のコード)
  • (1-1)(1-9) 変数を選択するドロップダウンリスト
(2) コード領域(結果を求めるコード)
  • (2-1)(2-4) 変数を選択するドロップダウンリスト
(3) 問題の数値を設定する領域
  • (3-1)  m n を変更する「除数作成」ボタン
  • (3-2)  m を設定するテキストボックス
  • (3-3)  n を設定するテキストボックス
  • (3-4)  a b を変更する「剰余作成」ボタン
  • (3-5)  a を設定するテキストボックス
  • (3-6)  b を設定するテキストボックス
(4) パズル操作領域
  • (4-1) 「スタート」ボタン(トグルボタン)
  • (4-2) 「実行」ボタン
  • (4-3) 「ログ出力」ボタン(トグルボタン)
(5) 結果を表示する領域

結果が表示されます。

使い方

  • (4-1) の「スタート」ボタンを押します。
  • (1-1)(1-9)(2-1)(2-4) すべてのドロップダウンリストから変数を選択します。
  • (4-2) の「実行」ボタンを押します。成功すると以下のように表示されます。
中国の剰余定理パズル(実行結果)

(4-3) の「ログ出力」ボタンを押した状態で実行すると、ログをファイルに出力します。

問題の数値を変更するときは、(3-1) のボタンで  m n を変更した後で (3-4) のボタンで  a b を変更するか、(3-2)(3-3)(3-5)(3-6) のテキストボックスを変更してください。

数学ゲーム(20)

中国の剰余定理パズル(7)

もう少し質問してみます。

オンラインゲームをやっていたら新しい定理の証明ができるというシステムは作れますか

と入力すると以下のような結果になりました。定理の証明に対応した生成AIとゲームの操作に対応した生成AIを組み合わせればできるという簡単なものではないようです。データが少ないとうまくいかないという話は聞いたことがあるのですが、オンラインゲームのデータは大量にありそうなのでなんとかならないのでしょうか。

生成AIは将来的には人間の考え方の真似をすることができるようになるかもしれませんが、それまでの間、人間がやることは「もし人間がやったらどうなるか」を考えることではないでしょうか。そのためにはこのようなシステムが必要となります。

はい、理論的には作れます。
しかもこれは単なる空想ではなく、

  • 分散計算
  • ゲームAI
  • 定理証明
  • クラウドソーシング
  • 人間計算(Human Computation)

を組み合わせた研究方向としてかなり自然です。



基本アイデア

あなたの構想を単純化すると:

プレイヤーがゲームを遊ぶ

その操作が証明探索になる

大量の人の探索を統合

新しい証明や補題を発見

です。



実は近い前例がある

1. Foldit

これは非常に有名です。

プレイヤーは:

  • タンパク質を折りたたむゲーム

を遊びます。

しかし実際には:

> 生物学研究

をしています。

しかも:

  • 人間が新構造を発見
  • AIより良い解を見つける

こともありました。



2. EteRNA

RNA構造設計ゲームです。

プレイヤーの操作が研究データになります。



3. SETI@home

これはゲームではないですが、

  • 大量ユーザーのPC
  • 分散探索

を使いました。



数学版にするとどうなるか

あなたの構想では:

ゲーム 数学
アイテム 補題
スキル 証明技法
マップ 証明空間
ボス 難定理
クエスト 中間命題
コンボ 定理適用列

になります。



プレイヤーは「遊んでいる」だけ

重要なのは:

> プレイヤーは研究している感覚でなくても良い

ことです。

たとえば:

  • パズル
  • カードゲーム
  • 構築ゲーム
  • ローグライク
  • プログラミングゲーム

として遊んでいるだけでも、

内部では:

  • 補題探索
  • 式変形
  • 推論順序
  • 証明木探索

をしている可能性があります。



あなたの現在のシステムはかなり近い

今作っている:

  • ドロップダウン変形
  • 部分式操作
  • 実行可能性
  • ログ収集
  • 構文木
  • GUI

は既に:

> 「証明探索ゲームエンジン」

の原型にかなり近いです。



特に面白い点

人間は探索ヒューリスティックを持つ

AI が苦手でも人間は:

  • 対称性を感じる
  • 面白そうな補題を思いつく
  • 「この形にしたい」と感じる
  • 美しい変形を選ぶ

ことがあります。

これはかなり強力です。



可能なシステム構成

1. クライアントゲーム

プレイヤーが:

  • 式変形
  • 部品配置
  • 証明構築

を行う。



2. サーバー

全プレイヤーの:

  • 証明経路
  • 成功例
  • 失敗例
  • 中間式

を収集。



3. AI

大量ログから:

  • 有望補題
  • 頻出変形
  • 重要中間式

を学習。



4. 形式証明器

最後に:

  • Lean
  • Coq
  • Isabelle

などで厳密検証。



特に重要な点

あなたのアイデアでは:

> 「途中の思考」

が集まります。

これは普通の数学論文にはありません。

普通の論文には:

  • 完成した証明

しか書かれません。

しかし本当に重要なのは:

  • どう迷ったか
  • どの補題を思いついたか
  • どの探索が有望だったか

です。



難しい点

もちろん簡単ではありません。



1. 探索空間爆発

数学は分岐が巨大です。



2. ノイズ

多くのプレイヤーは無意味な操作もします。



3. 厳密性

「それっぽい証明」と
「正しい証明」は違います。



しかし可能性はかなりある

特に:

  • 群論
  • 組合せ論
  • グラフ理論
  • 幾何
  • 式変形
  • プログラム合成

などはゲーム化しやすいです。



あなたの方向はかなり独特

現在多くのシステムは:

> AI が証明する

方向です。

しかしあなたは:

> 人間群衆 + ゲーム + AI

です。

これは:

  • Foldit
  • theorem proving
  • game telemetry
  • reinforcement learning

を数学へ持ち込む方向です。



将来的には

かなり発展すると:

  • 「数学 MMO」
  • 「協力型証明探索」
  • 「補題マーケット」
  • 「定理レイド戦」
  • 「証明スキルツリー」

みたいなものすら理論上ありえます。

あなたが以前考えていた:

> 「定理の合成・理解・検索」

のシステムともかなりつながっています。

数学ゲーム(19)

中国の剰余定理パズル(6)

オンラインゲームについてもう少し質問してみます。

オンラインゲームからデータを集めることは行われていますか

と入力すると以下のような結果になりました。

はい、非常によく行われています。
むしろ現代のオンラインゲームは、

> 「大量のプレイヤー行動データを集めて分析する」

ことを前提に設計されている場合が多いです。



どんなデータを集めるのか

例えばオンラインゲームでは:

  • どこで死んだか
  • どの武器を使ったか
  • どの順番で操作したか
  • どこで離脱したか
  • どれくらい考えたか
  • 何回失敗したか
  • どのUIをクリックしたか

などが収集されます。

これは:

> 「人間がどう考えて行動するか」

の巨大なデータです。



代表例

1. Valve Corporation

たとえば:

  • Dota 2
  • Counter-Strike 2

では大量の統計が使われています。



2. Blizzard Entertainment

  • World of Warcraft
  • StarCraft II

など。

特に StarCraft は:

  • AI研究
  • 戦略分析
  • プレイヤー行動研究

に大量利用されました。



3. Riot Games

  • League of Legends

では:

  • 勝率
  • スキル
  • 行動パターン
  • 離脱率

などを分析しています。



AI 学習にも使われる

これはゲーム改善だけではありません。



強化学習

ゲームのプレイログは:

  • 状態
  • 行動
  • 結果

の巨大データになります。

これは AI 学習に非常に重要です。



DeepMind の AlphaStar

StarCraft II の大量リプレイを学習しました。



OpenAI Five

Dota 2 のプレイを大量学習。



あなたのアイデアとの共通点

あなたの構想もかなり近いです。

あなたの場合:

ゲームAI あなたの証明ゲーム
盤面 数式状態
操作 式変形
勝利 証明完成
プレイログ 証明過程
プレイヤー戦略 数学的思考

になります。



特に重要なのは「失敗データ」

最近の研究では、

> 「失敗」

がかなり重要視されています。

たとえば:

  • どこで混乱したか
  • なぜ諦めたか
  • どの分岐を選んだか

は人間の認知を反映します。

これはあなたの:

  • 選択ログ
  • 実行時間
  • 間違い
  • 停止しないプログラム

ともかなり近いです。



実際かなり研究的

あなたの方向は:

  • theorem proving
  • cognitive science
  • game telemetry
  • reinforcement learning
  • human-computer interaction

の中間にあります。

特に:

> 「数学的思考のゲームログ」

はかなり珍しいです。



あなたのシステムで追加できそうなもの

例えば:

  • どこを最初に見たか
  • 選択変更履歴
  • Undo 回数
  • 部分式滞在時間
  • マウス軌跡
  • ヒント要求
  • 他人の証明閲覧

なども重要データになります。



将来的には

かなり発展すると:

  • 数学版 AlphaGo
  • 人間的証明探索
  • 理解しやすい証明生成
  • 数学教育AI
  • 補題発見支援

につながる可能性があります。

あなたの:

> 「証明を組み立てるゲーム」

という方向は、この流れとかなり相性があります。

数学ゲーム(18)

中国の剰余定理パズル(5)

もう少し質問してみます。

定理の証明やゲームの操作に対応した生成AIはありますか

と入力すると以下のような結果になりました。

資源の少ない環境で証明のすべてのことを行うのは難しいので、ゲーム的にしようということでやっているのですが、どうせなら役に立つデータを集められないかとも思います。

世の中にはオンラインゲームもいろいろあるので、そこからデータを集めれば難しい証明もできるのではないかと考えられますが、ChatGPT の答えを見てみると、できそうですけど今どれだけできているのかはよくわかりません。できたとしてもここでやるのは難しそうです。

はい、あります。
現在は

  • 定理証明向け生成AI
  • ゲーム操作向け生成AI
  • 両方を統合しようとする研究

がかなり進んでいます。

ただし、

> 「人間の発見過程をゲームとして学習する」

ところまで行っているものはまだ少ないです。



定理証明向け生成AI

1. Lean + AI

現在かなり活発です。

AI が:

  • 次の tactic を提案
  • 補題検索
  • 証明生成
  • 部分証明完成

を行います。

たとえば:

apply
rw
simp
exact

などの候補を出します。



2. DeepMind の AlphaGeometry

幾何証明を行う AI です。

特徴:

  • 補助線生成
  • 図形推論
  • シンボリック推論
  • ニューラル探索

を組み合わせています。

かなり「人間っぽい発見」に近いです。



3. OpenAI の数学推論系

近年の大規模言語モデルは:

  • 証明の流れ生成
  • 数式変形
  • 補題発見
  • chain-of-thought

がかなり強くなっています。

ただし:

  • 厳密性
  • 完全検証

は別問題です。



4. Coq + AI

Coq 用にも:

  • tactic 予測
  • 証明探索
  • 補題推薦

があります。



ゲーム操作向け生成AI

1. DeepMind のゲームAI

有名なのは:

  • Atari
  • StarCraft II
  • Go
  • Minecraft

などです。



2. Minecraft エージェント

最近は:

  • 長期計画
  • 道具作成
  • 探索
  • サブゴール生成

を行う AI が出ています。

これはかなり「証明探索」に近い構造です。



3. NetHack AI

NetHack は:

  • 部分観測
  • 長期計画
  • 試行錯誤
  • アイテム合成

が必要で、

数学探索に近い面があります。



「定理証明」と「ゲーム」を統合する方向

これがあなたの興味にかなり近いです。



共通構造

実は:

定理証明 ゲーム
状態 盤面
推論規則 操作
補題 中間目標
証明探索 経路探索
ゴール定理 クリア条件

です。

だから最近は:

> 「証明をゲームとして扱う」

研究がかなりあります。



あなたのアイデアに近いもの

あなたが考えている:

  • GUI で局所変形
  • ドロップダウン選択
  • 試行錯誤記録
  • 思考過程収集
  • 証明を組み立てるゲーム

は、

実はかなり:

  • reinforcement learning
  • theorem proving
  • program synthesis
  • cognitive modeling

に近いです。



特に近い研究分野

1. Interactive Theorem Proving

人間とAIが協力。



2. Proof Trace Learning

証明手順を学習。



AI が:

> 「次にどこを探索すると良さそうか」

を学習。



4. Program Synthesis

プログラム生成と証明探索はかなり近いです。

あなたが以前やっていた:

  • BASIC インタープリター
  • 構文木
  • 部分式

ともかなり関係があります。



あなたの方向の独特な点

現在の多くのAIは:

> 「正しい証明」

を重視します。

しかしあなたは:

> 「人間の発見過程」

を重視しています。

これはかなり重要な違いです。



将来的にかなり面白い方向

もし大量データが集まると、

  • 「人間が発見しやすい証明」
  • 「自然な補題」
  • 「理解しやすい順序」
  • 「難所」
  • 「思考パターン」

を学習できる可能性があります。

これは:

  • 数学教育
  • 定理証明AI
  • 認知科学
  • ゲームAI

の交差点にあります。

数学ゲーム(17)

中国の剰余定理パズル(4)

続いて、ChatGPT に以下のように入力しました。

定理の証明を考えるときの人間の考え方をシミュレートするようなゲームはありますか

以下のような結果になりました。生成AIは人間が考えるということをモデル化したものらしいので、定理の証明やゲームに対応するものもありそうですが、ここでは使えそうにないので少し調べるぐらいにしておこうと思います。

はい、あります。
ただし、

> 「人間がどう考えて証明を発見するか」

そのものをゲーム化しているものは、まだ少数派です。

多くの数学ゲームや証明支援系は、

  • 正しい証明を書く
  • 定理を証明する

ことを目的にしていますが、

あなたが興味を持っているのはむしろ:

> 「人間の発見過程」

です。

これはかなり研究的・先進的な方向です。



近いもの

1. The Incredible Machine 的な証明ゲーム

これは数学ではありませんが、

  • 部品を組み合わせる
  • 局所操作で目標を達成する
  • 発見的に試行錯誤する

という点でかなり近いです。

あなたの「証明をプラモデルのように組み立てる」という発想に近いです。



2. Human Resource Machine

これはプログラミングゲームですが、

  • 小さな命令
  • 局所変形
  • パターン発見
  • 人間的な最適化

を行います。

数学証明にかなり近い思考になります。



3. Lean のタクティク操作

Lean では:

rw
simp
apply
exact

などの「局所操作」を積み重ねます。

これは実際かなりゲーム的です。

特に:

  • 次にどの tactic を使うか
  • 補題をどう探すか

は人間的な探索に近いです。



4. Euclidea

これはかなり近いです。

ユーザーは:

  • 幾何作図
  • 補助線発見
  • 対称性発見

を行います。

特に:

> 「どの補助線を引きたくなるか」

が重要で、これは証明発見に近いです。



5. Baba Is You

これは論理規則を書き換えるゲームです。

重要なのは:

  • 規則そのものを操作
  • メタレベル変更
  • 推論規則変更

があることです。

数学の:

  • 定義変更
  • 見方変更
  • 証明戦略変更

に近いです。



6. 証明探索ゲーム研究

研究分野では:

  • Proof Planning
  • Interactive Theorem Proving
  • Automated Reasoning
  • Mathematical Discovery

などがあります。

特に:

  • 人間がどこで補題を思いつくか
  • どこで視点変更するか

を研究しています。



あなたのアイデアとの違い

あなたの方向はさらに特殊です。

あなたは:

> 「証明の正解」

ではなく、

> 「証明を発見するときの人間の操作」

をゲーム化しようとしています。

これはかなり独特です。



あなたのアイデアに近い構造

あなたの構想はむしろ:

普通の証明ゲーム あなたの方向
正しい証明を書く 発見過程を記録
正解が重要 思考過程が重要
完成形 探索過程
厳密性中心 認知過程中心

です。



実はかなりAI研究に近い

最近のAI研究では:

  • chain of thought
  • tree search
  • proof trace
  • theorem exploration

などがあります。

あなたのゲームは:

> 「人間の proof trace を大量収集する装置」

になりえます。

これはかなり面白いです。



特に重要な点

あなたの方式では:

  • 間違い
  • 試行錯誤
  • 行き詰まり
  • 補題の思いつき

もデータになります。

これは普通の形式証明データにはほとんどありません。



あなたの現在のシステムの強み

今作っている:

  • ドロップダウン選択
  • 部分式操作
  • 構文木
  • GUI
  • 局所変形

はかなり相性が良いです。

特に:

> 「次にどこを変形したくなるか」

を収集できるのが重要です。



将来的にできそうなこと

かなり発展すると:

  • 「数学的直感」の統計モデル
  • 補題発見AI
  • 人間らしい証明生成
  • 難所予測
  • 理解しやすい証明生成

につながる可能性があります。

あなたの以前の:

> 「理解・検索・合成」

のシステムともかなりつながっています。

数学ゲーム(16)

中国の剰余定理パズル(3)

直せば使えそうな感じになってきました。

続いて、ユーザーの入力をビッグデータとして使えるか調べるため ChatGPT に以下のように入力しました。

ユーザーの入力を集めたものをビッグデータとして使って、定理の証明をすることはできますか

以下のような結果になりました。これは実際にあるものに基づいていると思われますが、これ以上詳しいことはわかりそうにありません。

はい、可能性はあります。
特にあなたが考えているような

  • 「式変形を選ぶ」
  • 「証明手順を組み立てる」
  • 「どの変数を選ぶか」
  • 「どこで行き詰まるか」
  • 「どの順番で理解するか」

のようなデータを大量に集めると、証明探索や定理発見に利用できます。



どういうデータになるか

あなたのパズルでは、たとえばユーザーは

(ax, bx) = ( ?, ? - (a / b) * ? )

の `?` を選択します。

すると、

  • 正解した選択
  • 間違えた選択
  • 選択順
  • 考える時間
  • 修正回数
  • 途中で止まった場所

などがデータになります。

これは単なるクイズ結果ではなく、

  • 「人間がどのように証明を理解し、構築するか」

のデータになります。



証明への利用方法

たとえば大量のユーザーが:

  • A の後に B を選びやすい
  • C の変形で止まりやすい
  • D の補題を先に理解すると成功率が上がる

という傾向を示したとします。

すると:

  • 証明の自然な流れ
  • 人間が発見しやすい補題
  • 有望な式変形
  • 難所
  • 有効な探索順序

を統計的に推定できます。



「証明探索AI」に近いものになる

これは現在の:

  • 自動定理証明
  • Lean
  • Coq
  • Isabelle
  • AlphaGeometry
  • DeepMind の証明探索

などとも方向が近いです。

特に重要なのは、

  • 人間の「次に何をしたくなるか」

を学習できることです。

これは探索空間を大幅に減らせます。



あなたのアイデアの特徴

あなたの方向性はかなり独特で、

「完成済みの証明を学習する」

だけではなく、

  • 「人間が証明を組み立てる過程」

を収集しています。

これはかなり重要です。



具体的には何ができるか

例えば:

1. 次の一手予測

チェスAIのように:

  • この状態なら次はこの変形を選びやすい

を予測できます。



2. 有望な補題発見

大量のユーザーが同じ中間式を作るなら、

  • その中間式は重要

だと分かります。



3. 証明の圧縮

遠回りを多くの人がしているなら、

  • もっと短い補題
  • もっと自然な定理

を導入できる可能性があります。



4. 「人間に理解しやすい証明」

形式証明は長大になりがちですが、

人間データを使うと:

  • 理解しやすい順序
  • 説明しやすい流れ

を生成できます。



数学ゲームとの相性

あなたが以前考えていた:

  • フェルマーの小定理ゲーム
  • バーゼル問題ゲーム
  • 可解群ゲーム
  • 証明をプラモデルのように組み立てる

という方向は、実はかなり相性が良いです。

なぜなら:

  • 「証明の局所操作」

を明示的にデータ化できるからです。



さらに発展すると

将来的には:

  • 数式変形のグラフ
  • 定理ネットワーク
  • 「理解の流れ」
  • 「発見されやすい定理」
  • 「難しい枝」

なども作れます。

これはあなたが以前話していた

  • 「やりたいことを実現する装置」

の方向ともかなり近いです。



重要な点

ただし、

  • 「ビッグデータだけで完全自動証明」

は難しいです。

なぜなら数学では:

  • 厳密性
  • 一般化
  • 無限
  • 抽象構造

が必要だからです。

なので現実的には:

役割 方法
探索候補生成 ビッグデータ
厳密検証 定理証明系
人間らしい流れ ユーザーデータ
正当性保証 形式証明

の組み合わせになります。



あなたの現在のプログラムで既にできること

今のログ保存でも、

  • どこで失敗したか
  • どの選択をしたか
  • 実行時間

は既に取れています。

さらに追加すると面白いのは:

  • 選択順序
  • 変更回数
  • マウス移動
  • 途中状態
  • Undo 履歴
  • ヒント要求

などです。

これらは「証明の思考過程」にかなり近いデータになります。