巨大数研究 Wiki
Advertisement

SCGの限界を構成するグラフ列の候補

Haskell をやっていたらいつの間にかに数学にはまってた人です。カタカナではヘキサープと呼んでください。

自分史

2016: たぶん、不可説不可説転とか、その辺りから巨大数を知った。巨大数論に載っている表記を、片っ端から、関数形式で定義しようとしたり、 Haskell で実装しようとしたりしていた(残骸)。別の趣味へと流れていった。

2019-2021: 巨大数 Advent Calender 2018 を発見して再燃する。そこからの活動は知っての通りである。

子記事

テンプレート

お気に入り

メモ

今日の何か

issue が投稿された日時を x として、その issue についた最後のコメントが投稿された日時を y としよう。今日の日時を z としよう。 2 * (y - x) + day 30 <= z - x の時に ping を行う bot はどうだろうか?

"A Strongly Normalising Curry-Howard Correspondence for IZF Set Theory" が IZF 集合論と同じ強さを持つ型理論を実装している。構成的かどうかには疑問符が付くが。そして、そのアイデアを coq-contribs/izf で実装している。 "the intuitionisitic version of Hilbert's choice operator" なるものが関わっているらしい。

ここでの "the intuitionisitic version of Hilbert's choice operator" は、 HoTT 的には、 Natural_Number(i) : Universe(i) とし P : Universe(i) -> Universe(j) とし epsilon(i)(j) P : Natural_Number(i) -> Universe(i) である。そして、 P : Universe(i) -> Universe(j) とし || Σ { X : Universe(i) } { P ( X ) } || -> || Σ { n : Natural_Number(i) } { P ( epsilon(i)(j) P n ) } || である。

他のウィキ

外部リンク

  • Hexirp/googology - ブログ記事の下書き兼バックアップのリポジトリ。他にもいろいろあるよ。

バシク行列システム (BMS) 関係。

Advertisement