2026-01-04

Lean

#lean4

Lean カーネルがどんなものか？ Lean 4 に関して明示的な記述が見つからない。Lean 3 では、カルネイロ〈Mario Carneiro〉の論文があったが今は見当たらない。

大筋は Lean 3 のときと変わらないと思う。

(replyに続く 1/n)

#lean4

つまり、 ZFC + ωIC のなかで、ωTU + PU + λΠ + CIC を解釈できる（頑張れば）。

λΠ:

Deduktiエンコーディングとは、

Coqなどの証明支援系で作成された証明を、LambdaPiModuloという形式手法に基づいたDeduktiというシステム上で表現・検証（エンコード）する技術で、特に証明の検証可能性（証明検証器への入力）や計算可能性を高めるために、リライティング（書き換え）能力を駆使して行われる複雑な形式化プロセスを指します。これは、異なる証明系間で証明を相互運用したり、証明の信頼性をより低レベルで保証したりするために用いられます。

2-theories

2-theoriesとは...

メモ

さくらインターネット

下り通信料金が無料かつ、月額固定で計算できる仮想サーバー(円ベース)

ハウジングホスティングだけではなく、他のパブリッククラウドやオンプレミスもプライベート接続可能なネットワークサービス

低レイヤでクラスタ化できるため、オーバーヘッドを軽減できるGPUサービス

汎用ミドルウェア機能でクラスタリング(レプリケーション)できるデータベースサービス

大規模災害の影響を同時に受け辛い東京と石狩構成

など、伸びてるにはちゃんと理由がある特色がいくつかございますので、知りたい方はいつでもDMいただけますと説明に馳せ参じます！！是非！！！