2024.09.05
https://gyazo.com/984ab10e7c592ae1257af0666c08232f
前：
2024.09.04
後：
2024.09.06
#日報
思った
こんなに素晴らしい人々のお手を煩わせて申し訳ない…と思うことが増えた
おめでとう！
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/G.C3.B6del's.20Incompleteness.20Theorem
第2不完全性定理
の
Lean 4
での形式化についてのアナウンス
メモ
J. Brighton; "Cut-elimination for GLS using the terminability of its regress process"