RIMS Set Theory Workshop 2023 のウェブサイトを更新しました:
tenasaku.com/RIMS2023/
本日 (9/23) 中に RIMS に色々の書類を提出します。

We're pleased to announce the first official release of Lean 4!
Release notes: github.com/leanprover/lean4/re
Post on the community blog about future release cycles: leanprover-community.github.io

precompact は premium compact の略だったのか(違

プレミアムコンパクトSUV

なる自動車の広告文句を観測。
ついつい

premium compact

というトポロジーの用語はあるか、なかったら作ってやろうか、などと邪念がよぎる。

実務家教員がいるなら
$p$進務家教員もいるはず

Show thread

実務家教員がいるなら
複素務家教員もいるはず

Show thread

実務家教員がいるなら
虚務家教員もいるはず

実務家教員の定義が何なのか、そんなことたぶん誰も知らん

Show thread

なるほど〜ということは中世のヨーロッパでは決闘があったりしたから、取っ組合がuniversityになってもよかったわけか(謎

チャールズ・H・ハスキンズ『大学の起源』という本を読んでいる。大学を意味する「ユニバーシティ」は語源的に「ユニバース」や「ユニバーサル」には関係がなく、いまでいう「ユニオン」つまり学生と教師の組合というところから発生しているらしい。中世のヨーロッパでは「ユニバーシティ」は別に鍛冶屋の組合でもパン屋の組合でもよかったらしいぞ。

Leanの勉強会面白かったです。

勉強になりました。途中試行錯誤してなんとか証明ができたのに、どうやったらこれが自分で作れるのか考え方が全然わからんかった序盤のところ、見たことのある俳人が現れて、わしが求めているいい感じの説明をくださったのでよくわかった。

Leanの証明の書き方を否定とからめるのがさっぱりわかってなくて手間取ったのでした。その後よりも序盤のその否定の部分がわしには難しかったです。

Show thread

Hey there, we've got a whole bunch of folks from Japan hanging out here on our Mastodon server, . But don't let that hold you back - we're open to everyone, no matter what language you speak. Feel free to chat about anything from the serious world of math to the funniest math-related jokes or even just a friendly chit-chat. We can't wait to hear from you!

Show thread

This Mastodon server has many Japanese users on site, but of course we welcome any language speakers. Math topics, math-related gags, and chit-chat are all welcome.

Ce serveur Mastodon compte de nombreux utilisateurs japonais, mais nous accueillons bien sûr tous les locuteurs de langues. Les sujets mathématiques, les gags liés aux mathématiques et le bavardage sont tous les bienvenus.

Lean 4の勉強会にオンライン参加しています。

「立体射影模型」と「懸垂面螺旋面変形模型」のキットを用意しています。

Show thread

来月の9/2に「編み紙工作ワークショップ (理論解説付き)」のタイトルで講演します。申込みは本日までです!!
sugaku-bunka.org/

長文のときにトゥート入力画面が壊れてしまうことを、つどいさんのトゥートで知りました。

確かになる! 何年こうなっていたんだ! ←

なんとかなおします!


mathtod.online/web/@tsudoionli

Show older
Mathtodon

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