論計舎
問い探しから伴走する数学のオンライン私塾
気になったことを数学の問いにして、自分で確かめたい人のための私塾です。答えがすでに知られているか、まだ誰も知らないかは、条件にしていません。
たとえば「Lean で証明が通れば、その定理は正しいと言えるのか」が気になったなら、何が分かれば答えになるのかを一緒に言葉にします。そのあと、既知の結果を調べたり、自分で証明を試みたりします。
セッション・コースでは、90分の映像通話を月2回行います。受講者一人ひとりについて、その人の考え方と書き方を講師が覚えていられる人数として、定員を3名にしています。
専門は論と計の科学です。数理論理学と理論計算機科学をこう呼んでいます。講師がどう考え、どう説明するかは、公開している動画で分かります。
動画で見る
Lean は数学の土台より強い。では、何を根拠に信頼するのか｜形式検証入門3
証明支援系が「正しい」と言うとき、何が保証されているのか。
Lean は「Lean は無矛盾」を証明できない。「Lean の中」とはどこか｜形式検証入門2
不完全性定理を、証明支援系の中から見る。
エンジニアのための計算理論入門「決定不能性とは何か」
ライスの定理から、静的解析ツールが近似でしかありえない理由を見る。
講師について
川井 新
論計舎代表・講師の川井 新です。論と計の科学、なかでも論理と計算の関わりを在野で研究しています。哲学的論理学にも関心があります。RIMS（京都大学数理解析研究所）の共同研究で2回口頭発表し、『RIMS講究録』にも掲載されています。他の成果の一つに、中間論理のハイパーシーケント計算を Lean 4 で形式化した hyperseq-lean（共同研究、2026年8月公開）があります。
論計舎の前身のオルガノンクラスのころから、「論と計」を伝え、数学を独習できるようになるまでの補助輪になるつもりで、対話を中心に私塾を運営してきました。私も自分で立てた問いを研究しているので、受講者とも問いを立てるところから一緒に考えましょう。
指導したことのある分野は、微分積分学と線形代数（基本の数学）、数理論理学、理論計算機科学などです。ウィスキーと珈琲が好きです。