Inter-universal geometry と ABC予想 49

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

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

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

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

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

986(1): 2020/04/15(水)13:13 ID:QCk3Iyvt(2/3) AAS
>>985
そのプログラムの正当性はどうやって検証するの？