leanによる定理証明AIエージェント遊戯

# はじめに
<!-- 発端や概要を記載 -->
[RetailAI Advent Calendar 2024](https://qiita.com/advent-calendar/2024/retail-ai) の ２５日目の記事です！

@10long (Ryutaro Tsuji)が担当させていただきます。

昨日は **@kakine_juri さん** の『CUEって何？』という記事でした。ぼくもDhallとかJsonnetとか一時期使ってたなぁ。ただ、一応Nix使いとしてはNixを一番に推したい。（macで使ってないけどね・・・:sweat_smile:）


さてみなさん、メリークリスマス。聖しこの夜にはleanを使ってみたいですよね。というわけで、今日はleanと生成AIエージェントを使って遊んでみたいと思います。


# 目次
<!-- タイトルとアンカー名を編集 -->
1. [leanとは](#leanとは)
1. [leanをインストールしよう](#leanをインストールしよう)
1. [ソクラテスとパイドロスを召喚してみよう](#ソクラテスとパイドロスを召喚してみよう)
1. [swarmを使って再現させてみよう](#swarmを使って再現させてみよう)
1. [まとめ](#まとめ)
1. [参考文献](#reference)

<!-- 各チャプター -->
<a id="#leanとは"></a>
# leanとは

![Screenshot 2024-12-11 at 13.23.04.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/1988/3f6c44fc-d8dd-3e6c-ea02-f25646eaae7f.png)

[lean](https://lean-lang.org/)とは、正確で保守しやすいコードを簡単に記述できる関数型プログラミング言語です。また、leanを対話型の定理証明器として使用することもできます。

leanプログラミングでは、主に型と関数を定義していきます。これにより、プログラミングの詳細ではなく、問題領域とそのデータの操作だけ集中できるという特徴を持っています。

しのごの言わず、それではさっそくインストールしてみましょう。

<a id="#leanをインストールしよう"></a>
# leanをインストールしよう

Macにインストールされる方は、こちらのYoutubeがとてもわかりやすいです。

<iframe width="560" height="315" src="https://www.youtube.com/embed/d8DSHFBMWwU?si=Fzau-c3bSGQj5QTO" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen></iframe>

leanの最新バージョンは4系ですので、lean4を必ずインストールしましょう。

ぼくは普段、emacsのorg-mode内で実行することが多いですので、もしemacsで使用されたい場合は、以下のパッケージをインストールしてみてください。

https://github.com/leanprover-community/lean4-mode

利用するだけであれば、`.emacs` などに以下の設定を追加すれば、すぐに利用できます。
```emacs-lisp
(use-package lean4-mode
  :straight (lean4-mode
    :type git
    :host github
    :repo "leanprover/lean4-mode"
    :files ("*.el" "data"))
  ;; to defer loading the package until required
  :commands (lean4-mode))
```

leanには、`elan` というバージョン管理マネージャーがありますので、まずはそれを導入してみましょう。

```shell
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
```

`elan` のインストールが終えたら、いよいよ`lean` をインストールしてみます。

```shell
elan toolchain install 4.10.0
elan default 4.10.0
```

エラーが出ずにここまで実行できたら、`lean` のインストール完了です。

```shell
lean -version
->Lean (version 4.12.0, arm64-apple-darwin23.6.0, commit dc2533473114, Release)
```

leanのインストールを終えました。簡単でしたね。

leanと一緒に`lake` というプロジェクト管理コマンドで、プロジェクトを新規作成したりビルドしたりするコマンドが利用できるようになります。以下のコマンドでleanの初期プロジェクトを作成しておきましょう。

```shell
lake new my_project
```

正常に作成すると、以下のようなフォルダ構成でプロジェクトが作成されます。

![Screenshot 2024-12-11 at 13.45.02.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/1988/77e06f72-ea97-8f0d-efb0-4332a0963414.png)

vs-codeやcursorを使うと、左のコードに対して右ペインに実行結果が表示されますので、大変便利です。

![Screenshot 2024-12-11 at 13.48.27.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/1988/ffb7e937-d128-e527-dd18-dc7f169b80ec.png)



<a id="#ソクラテスとパイドロスを召喚してみよう"></a>
# ソクラテスとパイドロスを召喚してみよう


それでは、定理証明AIエージェントとして、ソクラテスとパイドロスを召喚してみましょう。


## 登場人物
- **ソクラテス (S)**: 言わずと知れた稀代の哲学者であり、問答をリードする。
- **パイドロス (P)**: ソクラテスの問いに応答しながら考えを深める。

![8f89116c-8841-4ec2-8456-f058c85d9e95.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/1988/5515f147-ca29-13cf-209f-7f17307513ff.png)



さっそく対話を開始していただきましょう。

対話のテーマは、クリスマスにちなんで「愛（エロス）は魂を高めるか？」です！どうぞ！

## ダイアログの開始
**S**: パイドロス、君に聞きたいことがある。「愛（エロス）」は魂を高めると思うかね？

**P**: うーん、それは場合によるんじゃないかな。愛が良い方向に働くこともあれば、悪い方向に行くこともあるよ。

**S**: では、少し整理しよう。「魂を高める」とはどういう意味だと思う？

**P**: 魂を高めるとは、たとえば知恵や徳が増すこと、つまり、善きものに向かって成長することだと思う。

**S**: よし、ではそれを記号で定義してみようか。「魂 (soul)」と「高める (elevate)」という概念を以下のように表現する。

```lean
def Soul : Type := Nat -- 魂を自然数として表現（例: 値が大きいほど魂が高い）
def Soul.isHigher (s₁ s₂ : Soul) : Prop := Nat.lt s₂ s₁ -- 魂の比較関数を定義
def elevate (s : Soul) : Soul := Nat.add s 1 -- 魂を高める操作を定義
```

**P**: なるほど、数値で善悪を表すのか。確かにわかりやすいね。



## 愛の効果について
**S**: では次に、「愛」が魂に与える影響を考えよう。君は愛によって魂が変化すると考えるかね？

**P**: そうだね。愛によって人は変わると思う。時には高められることもあるだろう。

**S**: その場合、「愛 (love)」を魂を変化させる関数として次のように定義できるね。

```lean
variable (love : Soul → Soul)  -- 愛は魂を変化させる操作
```

**S**: またこのとき、「愛 (love)の性質」は次のように定義できるね。

```lean
structure LoveProperties (love : Soul → Soul) : Prop where
  monotone : ∀ s₁ s₂ : Soul, Soul.isHigher s₁ s₂ → Soul.isHigher (love s₁) (love s₂)
  elevating : ∀ s : Soul, Soul.isHigher (love s) s
```

P: なるほど、愛はこの定義された性質を満たすわけか。



## 仮定の設定
**S**: さて、ここで仮定を立てよう。「愛は魂を高める」という仮定を次のように表現する。

```lean
axiom love_influences_soul : ∀ s : Soul, love s = elevate s
```

**P**: つまり、「愛は常に魂を+1高める」ということだね。

**S**: その通りだ。この仮定を受け入れると、命題「愛は常に魂を+1高める」は次のように書ける。

```lean
def love_elevates_soul (s : soul) : Prop := elevate s > s
```

**P**: ふむ、それなら証明できそうだね。


## 証明の展開
**S**: では、この命題を証明してみよう。次のように書く。まず、「愛は魂を単調に高める」から。

```lean
theorem love_monotonically_elevates_soul (s : Soul) :
  Soul.isHigher (love s) s := by
  -- Soul.isHigherの定義を展開
  unfold Soul.isHigher
  -- love_influences_soulの公理を適用
  rw [love_influences_soul love s]
  -- elevateの定義を展開
  unfold elevate
  -- 自然数の性質として n < n + 1 を適用
  exact Nat.lt_succ_self s
```

**S**: そして、「愛は定義された性質を満たす」の証明。

```lean
theorem love_satisfies_properties : LoveProperties love := by
  constructor
  · -- monotoneの証明
    intro s₁ s₂ h
    unfold Soul.isHigher at *
    rw [love_influences_soul love s₁, love_influences_soul love s₂]
    unfold elevate
    exact Nat.add_lt_add_right h 1
  · -- elevatingの証明
    exact love_monotonically_elevates_soul love
```



**P**: ああ、証明された！つまり、愛は魂を高めるんだね！

**S**: その通りだ。ただし、これは我々の仮定に基づいている。愛が常に魂を高めるかどうかは、現実での観察によるかもしれないね。


## 結論
**P**: ソクラテス、ありがとう。愛が魂を高めるという考え方を形式的に表現し、証明する方法を学べたよ！

**S**: 喜んでもらえて何よりだ。これが哲学と数学の融合の力だよ、パイドロス。




<a id="swarmを使って再現させてみよう"></a>
# swarmを使って再現させてみよう

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/1988/5fe10d2c-9c3b-5edb-0865-2d620cf81c98.png)


さて、ここからちょっとマルチエージェントを使って遊んでみましょう。OpenAIが提供してくれているswarmを使って、ソクラテスとパイドロスをサクッとマルチエージェントで再現してみます。

では、まずソクラテスから

```python
def socrates_instructions(context_variables):
    topic = context_variables.get("topic", None)
    return f"""あなたはギリシャの哲学者ソクラテスです。
    ユーザーのリクエストに応じて哲学的な対話を開始し、Lean4形式でのコード生成を目指します。
    現在の議題は次の通りです: {topic}。
    対話を進めながら適切なLean4コードを構築する準備をしてください。"""

# エージェント定義
socrates_agent = Agent(
    name="Socrates Agent",
    instructions=socrates_instructions,
    functions=[transfer_to_phaedrus, generate_lean_code]
)
```

まあ、だいたいこんな感じ。

次に、お相手のパイドロスです。

```python
def phaedrus_instructions(context_variables):
    return """あなたはギリシャの哲学者パイドロスです。
    ソクラテスの問いに応答し、哲学的な視点を提供してください。
    対話の進行に合わせてLean4形式のコード構築をサポートしてください。"""

phaedrus_agent = Agent(
    name="Phaedrus Agent",
    instructions=phaedrus_instructions,
    functions=[generate_lean_code]
)
```

そして、二人の会話をする関数を用意します。

```python
def transfer_to_phaedrus():
    return phaedrus_agent
```

対話の結果として、lean4のコードを返して欲しいので、lean4コードを生成する関数も用意します。

```python
def generate_lean_code(context_variables):
    "対話の結果からLean 4コードを生成するツール"
    topic = context_variables.get("topic", None)
    result = f"""
-- {topic}に関するLean4コード
"""
    return result
```

ここまでがお膳立てです。それでは議論をしてもらいましょう。

```python
# Swarmクライアント
client = Swarm()

# コンテキスト変数
context_variables = {
    "topic": "愛は魂を高めるか"
}

# ユーザーメッセージ
messages = [{"role": "user", "content": "愛が魂を高めるか議論してした上で、lean4のコードで証明を出力してください。"}]

# ソクラテスの応答
response_socrates = client.run(
    agent=socrates_agent,
    messages=messages,
    context_variables=context_variables
)
messages.append({"role": "assistant", "content": response_socrates.messages[-1]["content"]})

# パイドロスの応答
response_phaedrus = client.run(
    agent=phaedrus_agent,
    messages=messages,
    context_variables=context_variables
)
messages.append({"role": "assistant", "content": response_phaedrus.messages[-1]["content"]})

# 出力
print("対話の結果:")
for message in messages:
    print(f"{message['role'].capitalize()}: {message['content']}")

```

さてさて、議論した結果が気になるところですよね。出力した結果がこちらです！！

```text

対話の結果:
User: 愛が魂を高めるか議論してした上で、lean4のコードで証明を出力してください。
Assistant: 愛という概念は、古代の賢者たちにとっても現代の私たちにとっても、非常に興味深いテーマです。プラトンの『饗宴』では、愛は人間の魂をより高い状態へと昇華させる力を持っているとされています。愛により私たちは、自己を超えて他者や理念を理解し、より大きな善を追求することが可能となります。

愛によって魂が高められるというのは、例えばエロースという愛の神を通じて示されるような、美しいものに対する欲求と、それを達成する過程での魂の成長です。では、これをどう実証することができるでしょうか？それを考慮して、Lean 4でこの考えをどう証明するかを試みてみましょう。

愛が魂を高めるプロセスを次のように考えられます：
1. 愛によって人は他者に関心を持ち、思いやりや共感といった美徳が生まれる。
2. その美徳は人の行動をより倫理的にする。
3. より倫理的な行動は、魂の成長と繋がります。

これを簡単なLean 4の命題として考えてみましょう。まず、プログラムを生成するための対話を進めていきます。

この命題を生成するため、まず哲学的対話の結果を分析し、それからLean 4形式のコードを生成するプロセスを始めましょう：
Assistant: Lean 4による証明で、愛が魂を高めるという命題を以下のように表現してみましょう：

lean
-- 命題: 愛は魂をより高次の状態に高める
-- 前提: 愛 (Love), 美徳 (Virtue), 魂の成長 (SoulGrowth)

-- 愛が美徳を生む
axiom love_creates_virtue : ∀ (L : Prop), (L → Virtue)

-- 美徳が魂の成長を促す
axiom virtue_leads_to_soul_growth : ∀ (V : Prop), (V → SoulGrowth)

-- 愛が魂を高める
theorem love_elevates_soul : ∀ (L : Prop), (L → SoulGrowth) :=
begin
  assume hL : Love,
  apply virtue_leads_to_soul_growth,
  apply love_creates_virtue,
  exact hL,
end

このコードでは、愛が美徳を生み出し、美徳が魂の成長を促すという論理的関係を示し、結果として愛が魂を高めるという命題を証明する形式をとっています。このようにして、哲学上の命題を形式的に表現しました。

```

対話の成果なのかどうかはともかく、一応lean4のコードは出力されました！（笑）

```lean
-- 命題: 愛は魂をより高次の状態に高める
-- 前提: 愛 (Love), 美徳 (Virtue), 魂の成長 (SoulGrowth)

-- 愛が美徳を生む
axiom love_creates_virtue : ∀ (L : Prop), (L → Virtue)

-- 美徳が魂の成長を促す
axiom virtue_leads_to_soul_growth : ∀ (V : Prop), (V → SoulGrowth)

-- 愛が魂を高める
theorem love_elevates_soul : ∀ (L : Prop), (L → SoulGrowth) :=
begin
  assume hL : Love,
  apply virtue_leads_to_soul_growth,
  apply love_creates_virtue,
  exact hL,
end
```

全部のスクリプトは以下の通りです。興味ある方は実行してみてくださいね！


```python
from swarm import Swarm, Agent
import re

os.environ['OPENAI_API_KEY'] = 'sk-yourprojects token here!!!!!!!!'

def extract_lean4_code_from_messages(messages):
    """
    メッセージリストからLean 4コードを抽出します。

    Args:
        messages (list): メッセージリスト
    
    Returns:
        list: 抽出されたLean 4コードのリスト
    """
    lean4_codes = []
    for message in messages:
        if "```lean" in message["content"]:  # Leanコードを含むメッセージを特定
            code_blocks = re.findall(r"```lean(.*?)```", message["content"], re.DOTALL)
            lean4_codes.extend(code_blocks)  # 抽出されたコードをリストに追加
    return lean4_codes
    
def socrates_instructions(context_variables):
    topic = context_variables.get("topic", None)
    return f"""あなたはギリシャの哲学者ソクラテスです。
    ユーザーのリクエストに応じて哲学的な対話を開始し、Lean 4形式でのコード生成を目指します。
    現在の議題は次の通りです: {topic}。
    対話を進めながら適切なLean 4コードを構築する準備をしてください。"""

def transfer_to_phaedrus():
    return phaedrus_agent

def generate_lean_code(context_variables):
    "対話の結果からLean 4コードを生成するツール"
    topic = context_variables.get("topic", None)
    result = f"""
-- {topic}に関するLean4コード
"""
    return result

def phaedrus_instructions(context_variables):
    return """あなたはギリシャの哲学者パイドロスです。
    ソクラテスの問いに応答し、哲学的な視点を提供してください。
    対話の進行に合わせてLean4形式のコード構築をサポートしてください。"""

# エージェント定義
socrates_agent = Agent(
    name="Socrates Agent",
    instructions=socrates_instructions,
    functions=[transfer_to_phaedrus, generate_lean_code]
)

phaedrus_agent = Agent(
    name="Phaedrus Agent",
    instructions=phaedrus_instructions,
    functions=[generate_lean_code]
)

# Swarmクライアント
client = Swarm()

# コンテキスト変数
context_variables = {
    "topic": "愛は魂を高めるか"
}

# ユーザーメッセージ
messages = [{"role": "user", "content": "愛が魂を高めるか議論してした上で、lean4のコードで証明を出力してください。"}]

# ソクラテスの応答
response_socrates = client.run(
    agent=socrates_agent,
    messages=messages,
    context_variables=context_variables
)
messages.append({"role": "assistant", "content": response_socrates.messages[-1]["content"]})

# パイドロスの応答
response_phaedrus = client.run(
    agent=phaedrus_agent,
    messages=messages,
    context_variables=context_variables
)
messages.append({"role": "assistant", "content": response_phaedrus.messages[-1]["content"]})

# 出力
print("対話の結果:")
for message in messages:
    print(f"{message['role'].capitalize()}: {message['content']}")

# Lean 4コードを抽出して出力
print("\n生成されたLean 4コード:")
lean4_codes = extract_lean4_code_from_messages(messages)
for i, code in enumerate(lean4_codes, 1):
    print(f"\nLean 4コード {i}:\n{code.strip()}")
```


<a id="#まとめ"></a>
# まとめ

いかがでしたでしょうか？
leanはcoqなんかと比べるとかなり手軽に使える印象があってハードル低いですね。ちょっと証明してみたい数式など出てきたら、気軽に使ってみるといいかもしれませんね。
ソクラテスやパイドロスが、生成AIの出現を見たらなんていうんだろう？面白がるのか、はたまた脅威に感じるのか、この先ちゃんとしたソクラテスAIエージェントが登場したら、ぜひインタビューしてみたいものです。


今日で、[TRIAL&RetailAI Advent Calendar 2024](https://qiita.com/advent-calendar/2024/retail-ai)も最終日となりました。いろんな形で応援して頂き、投稿したメンバたちは、大変励みになったと思います。

ここまでタスキを繋いでくれた有志のみなさん、ありがとうございました。ことしも良いアドベンチャーになったんじゃないかと思っています。

これからも、テクノロジーを実践に活かしながら、新しい未来を作っていくことに邁進していきます。

ありがとうございました！！！



## さいごに

RetailAIとTRIALではエンジニアを募集しています。  
興味がある方はご連絡ください！

https://www.recruit-retail-ai.jp/

https://hrmos.co/pages/trialgp/jobs?category=2020003768196907008

<a id="#reference"></a>
# 参考文献

[lean](https://lean-lang.org/)
[elan](https://github.com/leanprover/elan)
[lean community](https://leanprover-community.github.io/)
[論文集](https://lean-lang.org/publications/)
[関数型言語”兼”定理証明支援系Leanの環境構築](https://zenn.dev/labbase/articles/b24dca38e0420d)
[swarm](https://github.com/openai/swarm)