Inter-universal geometry と ABC予想 49

[過去ﾛｸﾞ] Inter-universal geometry と ABC予想 49 (1002ﾚｽ)
上下前次1-新
抽出解除ﾚｽ栞

このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索歴削→次ｽﾚ栞削→次ｽﾚ過去ﾛｸﾞﾒﾆｭｰ

984(2): 2020/04/15(水)13:06 ID:/g+JzMtk(1/9) AAS
>>983
＞証明支援言語Coqが正しいことを、だれがどうやって保証しているのか？

Coqの正当性をCoqで検証すればいいんじゃね？

985(1): 2020/04/15(水)13:10 ID:/g+JzMtk(2/9) AAS
>>984
具体的に説明するか

Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと

カリー＝ハワード同型対応
外部ﾘﾝｸ:ja.wikipedia.org

987(1): 2020/04/15(水)13:13 ID:/g+JzMtk(3/9) AAS
>>984
具体的に説明するか

Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと

カリー＝ハワード同型対応
外部ﾘﾝｸ:ja.wikipedia.org