https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Implication/level/0
上記のLeanを用いたNatural Number GameのWorld: Implication Worldを解いてると、型で証明できそうな気はしてきたのですが、カリー=ハワード同型対応 (Wikipedia) には以下のような記述がありました。
論理 プログラミング 真 ⊤ トップ型 1 偽 ⊥ ボトム型 0
いままで、素朴なプログラミング言語では true, false はブーリアン型という認識だったのですが、急にトップ型とボトム型が登場しました。論理(数学)の真偽とプログラミングのtrue, falseは別物なのでしょうか? いままで同じようなものだと思い、それがブーリアン型だと思っていたのですが... なにか文脈が違うのでしょうか? それとも boolean = トップ型 1 | ボトム型 0
みたいなことでしょうか?
追記:
https://proofassistants.stackexchange.com/questions/4185/the-relationship-between-true-formula-and-types-in-the-curry-howard-correspond にも質問しました(やり取り中ですが、私の数学力が低くて承認できなさそうです)。質問の過程で英語版のWikipediaの内容が変わりました(回答者が英語版Wikipediaを編集しました。そもそも日本語版と英語版で異なっていましたが、大幅に書きかわりました)。