SnO₂WMaN @sno2wman@fedibird.com

救われたい / 早く殺してほしい

日報(2023.08.24)

https://scrapbox.io/sno2wman/2023.08.24

不完全性定理を研究したいという要求のどこに複素数と微積分と制御工学が必要になるのか真剣に考えて欲しい

なにかの記事で「数学基礎論希望の院試受験者の成績が著しく悪すぎて、議論に」というのを読んだが、それにこれからなる

人間はシャキっとすると疲れる。そのあまりに当然の事実を忘れて計画を立てた結果として大変困難な事態に陥っている。

日報(2023.08.23)

https://scrapbox.io/sno2wman/2023.08.23

日報(2023.08.22)

https://scrapbox.io/sno2wman/2023.08.22

明日はcoq-community/goedel及びRussel O'Connor; "Essential Incompleteness of Arithmetic Verified by Coq"を読みLean4に移植可能かどうかを見てみたい

https://github.com/coq-community/goedel

日報(2023.08.21)

https://scrapbox.io/sno2wman/2023.08.21

どうにかかろうじてマトモな見かけにはしたが、まだ不自然に縦長になってしまっている感はある

日報(2023.08.20)

https://scrapbox.io/sno2wman/2023.08.20

TypstのBibliographyが本当に意味不明の挙動をするっぽいのでこの一点のみで現状オフィシャルな場では使えないと思う

日報(2023.08.19)

https://scrapbox.io/sno2wman/2023.08.19

終わっている

日報(2023.08.18)

https://scrapbox.io/sno2wman/2023.08.18

日報(2023.08.17)

https://scrapbox.io/sno2wman/2023.08.17

一応`#include`はあるがオンラインエディターもあるということを加味するとそもそも複数ファイル分割を想定しているのか謎な気がする（`template.typ`を作るのは定石ではあるっぽいが）

Typstは快適なのだけどファイル分割の方法がよくわからない（どう頑張ってもbibliographyの部分で詰まる）ので全部1ファイルに纏めるしか無いと思うがこれをやるとpdfのプレビューがかなりボトルネックになってしまう

日報(2023.08.16)

https://scrapbox.io/sno2wman/2023.08.16

Typstの文書をGitHub Actionsでコンパイルして自動でGitHub Pagesにデプロイするアクションも組んだので，いつでも最新版を読むことが出来ます

https://sno2wman.github.io/incompleteness.txt/main.pdf