Follow

そういえばmathtodon.onlineって定理証明支援系の話題ないですね。そんな人気ないんだろうか。使えたら便利そうだけど。

· · Web · 1 · 0 · 1

@uy 学生時代Coqの授業にちょっとだけ出ましたが当時プログラミングに興味なかったので、あんまり響かなかった(途中で切った)んですよね~。概念をプログラムに焼き直すの結構大変そうなイメージです。

@yajidasu あ、授業であるんですね。補完機能とかバリバリ使えるならヒューマンエラーなしで定理作るのに集中できそうなイメージありますけど、なんだか敷居は高そうですね。(Coqインストールするところから大変)

@uy 流石にニッチな分野な気がするのでどの大学でもあるかは知らないですけどね~。今久しぶりにHP覗いたら結構講義資料とか充実してたので貼っておきます。
math.nagoya-u.ac.jp/~garrigue/

@yajidasu 数学基礎論とか集合論とか圏論とかに興味あって、関係ありそうだから定理証明支援系はなんだか面白そうとずっと思っていたんですが、ニッチなんですねー。ありがとうございます。やっぱり基本的にemacsなのかあ...

Sign in to participate in the conversation
Mathtodon

A Mastodon instance named Mathtodon, where you can post toots with beautiful mathematical formulae in TeX/LaTeX style.