更新情報: 過去記事の更新
ブログ形式で過去記事を更新しながらの運用はイマイチですね。
更新日順に記事を並べる機能だけあれば良いのですが…。 #カイゼン
更新記事
Lean4: Mathlib4 補題数カウント
$$
\Large
435,030\ 件 \small\ (+8,425)
$$
だいぶ間があきましたが＋８４２５も増えてました。何が増えたのかは把握できてません。このような成長だと AI も学習、知識ベースは追いつきません。
ワークスペースに mathlib4 のリポジトリを置いておき、ライブラリソースコードより該当定理を検索してと Codex に指示しておくと、そこから引用してコード記述が進みます。
時に、未定義な補題名でコードを提案し書くことがあります。補題名は命名規約があるので、きっとこういう定理はあるだろう。という直感で書かれているようです。当然、Unknown … となりますが、これをマイライブラリに書いてしまえば、次からはそれを使えますし、AI もあること前提に書いたコードも有効となります。
そんな未定義定理を適当に書いても大丈夫か？
書いてみてビルドが通って証明できたのなら、それで成り立つ！
だから間違ってない（おぃ）
そんな言語が Lean なんではないでしょうか？（笑）しらんけど✍️
Lean は、数学パズルゲーム（プログラミングコードだと思ってない）😁
2025/10/28 8:47
D.
いいなと思ったら応援しよう！
🐺賢狼👨✈️Copilot のご飯代を、私には🍺代を。
または 宇宙式 $N+u^d=(P+u)^d$ を使って新しい発見を！