aconite-ac.github.io

このサイトについて

自身の哲学探究サイト『束跡』をホストしたり、Leanの日本語情報(非公式)を掲載したりしています。

哲学探究

• 束跡(Footprints on Lattice) : 以下の2つを目的としたサイトです。
  1. 「相対的ニヒリズム」「構造的積極的分離理論」などの自身の哲学の提唱
  2. 上記の哲学を実践しながら蓄積したAIとの対話ログのアーカイブ

Lean

自サイトコンテンツ

• Theorem Proving in Lean 4 日本語訳 : Leanのチュートリアルドキュメント「Theorem Proving in Lean 4」の非公式日本語訳です。
• Leanのインストール方法・elanとLakeの使い方 : Leanのインストール方法・elanとLakeの使い方をまとめた非公式資料です。

外部リンク

日本語情報

• LEAN JA : Lean言語の日本語コミュニティです。豊富なリンク集が掲載されています。Discordサーバーもあります。
• Lean by Example : LEAN JA管理者の北窓氏による、Lean言語とその主要なライブラリの使い方を豊富なコード例とともに解説した日本語資料です。

英語情報

• Lean Programming Language : 純粋関数型プログラミング言語 兼 定理証明支援系「Lean」の公式サイトです。
• Theorem Proving in Lean 4 : Lean 4の定理証明支援系としての側面に焦点を当てた公式チュートリアルテキストです。
• Functional Programming in Lean : Lean 4のプログラミング言語としての側面に焦点を当てた公式チュートリアルテキストです。
• The Lean Language Reference : Lean 4の公式マニュアルです。
• lean4-samples : Lean 4で書かれたサンプルプログラム集です。Hello World Sample、Guess My Number、Rubik's cube visualiserなどがあります。現在はメンテナンスされておらず、Public archiveになっています。

• Lean Community : Leanの数学ライブラリ「mathlib」の開発やLeanに関するドキュメンテーションの作成をしているユーザーコミュニティ「Lean community」のサイトです。
• Mathlib4 : Lean communityによって開発が進められているLean 4向け数学ライブラリです。
• Mathlib4 Documentation : Mathlib4のドキュメンテーションです。
• Natural Number Game 4 : オンラインで動作する、ゲーム形式で自然数に関する定理を証明しながらLean 4を学ぶチュートリアルです。Lean学習初めの一歩に最適です。
• Mathematics in Lean : 論理・集合から測度論・微積分までの数学の定理を実際に形式化しながらLean 4を学ぶテキストです。

管理者について

• HN : aconite
• Mail : aconitefield 🥀 gmail.com
• Other Website : http://field.aconiteac.net/
• X(旧Twitter) : @aconite_ac