X
トップページ⇒数学
274コメント91KB
【Coq】コンピューターで証明しよう【コック】©2ch.net
■ このスレッドは過去ログ倉庫に格納されています
0152１３２人目の素数さん
垢版 |
2016/05/25(水) 23:39:51.15ID:fzY8lffh
omegaは基本的に掛け算には無力
プレスバーガー算術を対象としているから、らしい

simplは単に定義に従って簡約してくれる
よって>>149には適用できるが、>>148はmatchできなくて無理
0153１３２人目の素数さん
垢版 |
2016/05/26(木) 00:17:18.47ID:vUOIQwNh
できました！
2^10=1024 > 1000を使うのがポイントだったみたいです。

Require Import Omega.

Theorem multi_inf_gt4:
forall (x : nat), x>1 -> exists m : nat, x^m > 1000.
(* proof. *)
intro.
intro.
destruct x.
omega.

exists 10.

assert (S x>1 -> 2^10 <= S x^10).
intro.
apply (Nat.pow_le_mono_l_iff 2 (S x) 10).
auto.
auto.

change (S x > 1 -> 1024 <= S x ^ 10) in H0.
apply H0 in H.
omega.
Qed.

レスして下さった皆様、ありがとうございます。
次は実数でチャレンジするかも!?
0155１３２人目の素数さん
垢版 |
2016/05/27(金) 03:19:24.12ID:ItPB2mak
実数でもx>2の場合はできました。
x^10を原始的にxで割っていく方法です。　右辺が10000だったらどーするんだwww

Require Import Rbase.
Require Import Fourier.

Theorem multi_inf_gt6:
forall (x : R), x>2 -> exists m : nat, (Rpow_def.pow x m)>1000.
Proof.
intro.
intro.

exists 10%nat.

simpl.

apply Rmult_le_0_lt_compat.
fourier.
fourier.
apply H.

apply Rmult_le_0_lt_compat.
fourier.
fourier.
apply H.

apply Rmult_le_0_lt_compat.
fourier.
fourier.
apply H.

assert (2*/2*125=125).
apply Rinv_r_simpl_r.
discrR.
assert (forall (a b c d:R), a*b*c = a*(b*c)).
intros.
ring.
rewrite H1 in H0.
rewrite <- H0.
apply (Rmult_le_0_lt_compat 2 x (/2*125) (x*(x*(x*(x*(x*(x*1)))))) ).
fourier.
fourier.
apply H.

all: cycle 1.
apply x.
0156１３２人目の素数さん
垢版 |
2016/05/27(金) 03:25:03.30ID:ItPB2mak
assert (2*/2*(/2*125)=/2*125).
apply (Rinv_r_simpl_r 2 (/2*125)).
discrR.
rewrite H1 in H2.
rewrite <- H2.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*125)) (x*(x*(x*(x*(x*1))))) ).
fourier.
fourier.
apply H.

assert (2*/2*(/2*(/2*125))=/2*(/2*125)).
apply (Rinv_r_simpl_r 2 (/2*(/2*125)) ).
discrR.
rewrite H1 in H3.
rewrite <- H3.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*125))) (x*(x*(x*(x*1)))) ).
fourier.
fourier.
apply H.

assert ( 2*/2*(/2*(/2*(/2*125))) = /2*(/2*(/2*125)) ).
apply (Rinv_r_simpl_r 2 (/2*(/2*(/2*125))) ).
discrR.
rewrite H1 in H4.
rewrite <- H4.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*(/2*125)))) (x*(x*(x*1))) ).
fourier.
fourier.
apply H.

assert ( 2*/2*(/2*(/2*(/2*(/2*125)))) = /2*(/2*(/2*(/2*125))) ).
apply (Rinv_r_simpl_r 2 (/2*(/2*(/2*(/2*125)))) ).
discrR.
rewrite H1 in H5.
rewrite <- H5.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*(/2*(/2*125))))) (x*(x*1)) ).
fourier.
fourier.
apply H.

assert ( 2*/2*(/2*(/2*(/2*(/2*(/2*125))))) = /2*(/2*(/2*(/2*(/2*125)))) ).
apply (Rinv_r_simpl_r 2 (/2*(/2*(/2*(/2*(/2*125))))) ).
discrR.
rewrite H1 in H6.
rewrite <- H6.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*(/2*(/2*(/2*125)))))) (x*1) ).
fourier.
fourier.
apply H.
0157１３２人目の素数さん
垢版 |
2016/05/27(金) 03:29:56.38ID:ItPB2mak
fourier.
apply x.
apply x.
apply x.
apply x.
apply x.
Qed.

1<x<2の場合はどうするんだろう？
0159１３２人目の素数さん
垢版 |
2016/05/30(月) 01:07:49.80ID:nh+30MzG
1<x<2の場合は、lim[x->∞](1+1/x)^x=eをヒントにできないかな、と思っています。

今日のCoq：
Require Import Rbase.
Require Import Fourier.

Lemma l2:
forall (x y:R), y>1 -> x=1+1/y -> 1<x<2.
Proof.
intros.
rewrite H0.

assert (forall (a b:R), a<b -> 1+a<1+b).
intro.
intro.
intro.
fourier.

apply conj.

assert (1+0=1).
ring.

replace (1<1+1/y) with (1+0<1+1/y).
apply (H1 0 (1/y)).

all: cycle 1.
rewrite H2.
reflexivity.

all: cycle 1.
assert (0<1 -> 0<1/y -> 1/y*0<1/y*1).
intro.
apply (Rfourier_lt 0 1 (1/y)).
auto.
assert (1/y*0 = 0).
ring.
rewrite H4 in H3.
assert (1/y*1 = 1/y).
ring.
rewrite H5 in H3.
ここまでで、仮定が0 <1 -> 0<1/ y -> 0 <1/ y、
サブコールが0 < 1 / yで頓挫。。。
0161１３２人目の素数さん
垢版 |
2016/06/01(水) 20:28:33.76ID:Ih6s2JtZ
1<x<2　->　x^m>1000、こんな感じになりました。existの形では出来なかったです。
まず1<x<2　->　x^m>2^10を証明して、それから1<x<2　->　x^m>1000を証明しています。

Require Import Rbase.
Require Import Fourier.

Theorem multi_inf_gt7':
forall (x y:R), 1<x<2 ->
x=1+1/y ->
(Rpow_def.pow x (Z.to_nat (up y)))>2 ->
(Rpow_def.pow x ((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))))>2*2*2*2*2*2*2*2*2*2.
Proof.
intros.

rewrite Rdef_pow_add.
（↑を9回）

apply Rmult_le_0_lt_compat.
fourier.
fourier.
（↑を9回）

apply H1.
（↑を10回）
Qed.
0162１３２人目の素数さん
垢版 |
2016/06/01(水) 20:31:57.00ID:Ih6s2JtZ
Theorem multi_inf_gt7:
forall (x y:R), 1<x<2 ->
x=1+1/y ->
(Rpow_def.pow x (Z.to_nat (up y)))>2 ->
(Rpow_def.pow x ((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))))>1000.
Proof.
intros.

assert ((Rpow_def.pow x ((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))))>2*2*2*2*2*2*2*2*2*2 ->
(Rpow_def.pow x
((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))))>1000).
intro.
fourier.

apply H2.

apply multi_inf_gt7'.
apply H.
apply H0.
apply H1.
Qed.
0163１３２人目の素数さん
垢版 |
2016/06/01(水) 20:37:28.80ID:Ih6s2JtZ
仮定に使ってる(1+1/y)^y>2ですが、
これをCoqで証明するのは難しそうなので、
このへんにしておきます。
0164片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2016/07/04(月) 17:27:13.86ID:I+l74NfK
今考えていることを書きます。

１．都内でCoq大会を開きたい。ゲーム形式でCoqの技能を競う。
２．Coqの数式操作をGUIでできるようにしたい。部分数式ごとに適用できるタクティクを「見える化」したい。
３．Coq Twitter BotやCoq onlineを作りたい。
0165片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2016/07/04(月) 17:34:29.59ID:I+l74NfK
でもOCamlを勉強する時間がないんだ。
やらないといけないことが他にもあるし。
0167１３２人目の素数さん
垢版 |
2016/07/04(月) 20:23:53.31ID:lwP0CPv1
日本語の良いチュートリアルが欲しい。
インタラクティブなやつならなお良し。
0168１３２人目の素数さん
垢版 |
2016/07/04(月) 21:14:49.99ID:b2jsrh3I
>>164
onlineはproofwebやらjscoqやらあるしbotの方が面白そうだな
140字でどの程度のことができるのかわからんが
0171１３２人目の素数さん
垢版 |
2016/07/08(金) 09:21:21.88ID:LlF6GjmQ
proofwebでcoqを使うと、画面の右下にGentzenのproof treeを
表示してくれるのですが、その機能をローカルに自分のパソコンでも
使えるようにできるのですか？できるのでしたらやり方を教えてもらえないで
しょうか。
0173171
垢版 |
2016/07/09(土) 13:47:50.56ID:n5Zs2sWR
>>172
レスありがとうございます。でも今Linuxは無理です。
残念です。
0176１３２人目の素数さん
垢版 |
2017/06/18(日) 16:49:48.59ID:v2schHZM
苗■

405 ： 猫は唯の馬鹿 ◆MuKUnGPXAY [age] 投稿日：2011/04/09(土) 15:29:50.46
猫
0177￥ ◆2VB8wsVUoo
垢版 |
2017/06/18(日) 17:35:53.09ID:ze+BLRMV
★★★数学徒は馬鹿板をしない生活を送り、日頃から真面目に学問に精進すべき。★★★

￥
0190￥ ◆2VB8wsVUoo
垢版 |
2017/06/19(月) 05:24:06.21ID:pqzlCEdf
★★★数学徒は馬鹿板をしない生活を送り、日頃から真面目に学問に精進すべき。★★★

￥
0204１３２人目の素数さん
垢版 |
2020/02/24(月) 04:56:39.43ID:DY3MFCYd
>>7
> English speakerに前置きなく「コック」って言ったら誤解を産むよね
日本語話者にも開発者のCoquandの名前を「コカン」って呼んだら誤解生みそう

「Coqはコカンが生みました」

？？？？？
0208１３２人目の素数さん
垢版 |
2020/08/31(月) 18:29:37.56ID:5YDNY7qe
これでMathematicaみたいなことができるの？
0209１３２人目の素数さん
垢版 |
2020/08/31(月) 19:38:58.46ID:CK4NnquJ
>>207
それは翻訳じゃなくて詳細な機械証明をつけたことになるからいいんじゃね？

やれるもんならやってごらん（挑発）
0210１３２人目の素数さん
垢版 |
2020/09/01(火) 19:16:57.55ID:2qjbTlF5
1700
学コン・宿題ボイコット実行委員会@gakkon_boycott 9月1日
#拡散希望
#みんなで学コン・宿題をボイコットしよう
雑誌「大学への数学」の誌上で毎月開催されている学力コンテスト(学コン)と宿題は、添削が雑で採点ミスが多く、訂正をお願いしても応じてもらえない悪質なコンテストです。(私も7月号の宿題でその被害に遭いました。)このようなコンテストに参加するのは時間と努力の無駄であり、参加する価値はありません。そこで私は、これ以上の被害者を出さないようにするため、また、出版社に反省と改善を促すために、学コン・宿題のボイコットを呼び掛けることにしました。少しでも多くの方がこの活動にご賛同頂き、このツイートを拡散して頂ければ幸いです。
https://twitter.com/gakkon_boycott/status/1300459618326388737
https://twitter.com/5chan_nel (5ch newer account)
0212１３２人目の素数さん
垢版 |
2020/12/29(火) 18:10:40.92ID:L4ADUw+o
Coqとかのソフトウェアを理解して使えるようになるには，どんな本を読めばいいですか？
0213１３２人目の素数さん
垢版 |
2020/12/29(火) 19:37:12.97ID:dboOL2nl
本なら『Coq/SSReflect/MathCompによる定理証明』かな。実際に使って証明したいものを証明した方が良いと思うけど。
0214１３２人目の素数さん
垢版 |
2020/12/29(火) 20:13:39.22ID:L4ADUw+o
>>213
ありがとうございます．
その本は読んだことがあるのですが，何が書いてあるのかよくわかりませんでした．
その本を読むための予備知識はどんな本を読めばいいのでしょうか？
0215１３２人目の素数さん
垢版 |
2020/12/29(火) 22:12:44.60ID:dboOL2nl
Coqで何をしたいのかは分からないけど、数学の証明をしたいのなら命題論理とか述語論理の勉強をしたらいいと思うよ。
0217１３２人目の素数さん
垢版 |
2021/03/04(木) 23:54:49.26ID:5lNvn7IX
F x = If x < 10 then x else F (x - 1)

みたいな関数ってCoqでどう性質を証明しますか？ifの条件で場合分けしたいです

タクティックでcase ( x< 10)としても、
仮説にならないで、場合わけにならずに困っています。
0220１３２人目の素数さん
垢版 |
2021/04/18(日) 19:19:36.97ID:3tfcWKwp
Coqで日本語データを処理するプログラム書けますか？
Asciiは扱えるみたいです。
0221１３２人目の素数さん
垢版 |
2021/06/13(日) 11:30:42.81ID:yMfojtwc
https://www.iij-ii.co.jp/activities/programming-coq/coqt1.html
これの練習問題の2つ目が分からない。
＞問1. 任意の命題 A B C に対して、「A ならば B ならば C」ならば「B ならば A ならば C」が成り立つ。

要するにこれはB⇒Aが可能なら、前提条件からA⇒Cだと思ったけど。
どう書くの？全然分からん

Definition prop4 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C):=
fun A B C a b c => ?.
0222１３２人目の素数さん
垢版 |
2021/06/13(日) 12:05:53.03ID:lCrOJ5I2
>>221
Definition prop4 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C) :=
fun A B C f b a => f a b.
かな。f の型が (A -> B -> C) で、b の型が B で、a の型が A 。
「ならば」(->) は右結合だから、(B -> A -> C) の部分の括弧は外す事ができる。
0224１３２人目の素数さん
垢版 |
2022/01/12(水) 08:10:41.00ID:0y6QDPS2
コックむずい
0225１３２人目の素数さん
垢版 |
2022/01/24(月) 07:16:51.96ID:OmUr/Vw+
ムズいよねえ
もっと勉強しなくては
0226１３２人目の素数さん
垢版 |
2022/02/11(金) 01:30:20.50ID:92XxvpJY
　　　| ＼
　　　|Д｀)　ﾀﾞﾚﾓｲﾅｲ･･ｵﾄﾞﾙﾅﾗ ｲﾏﾉｳﾁ
　　　|⊂
　　　|


　　　　　♪　　Å
　　　♪　　　／ ＼　　　ﾗﾝﾀ ﾀﾝ
　　　　　　ヽ(´Д｀;)ﾉ 　　ﾗﾝﾀ ﾀﾝ
　　 　 　　　 (　 へ) 　　　ﾗﾝﾀ ﾗﾝﾀ
　 　 　 　 　　く 　　　　　　ﾀﾝ



　　　♪　　　　Å
　　　　　♪　／ ＼　　　ﾗﾝﾀ ﾗﾝﾀ
　　　　　　ヽ（;´Д｀）ﾉ　　ﾗﾝﾀ ﾀﾝ
　　 　 　　　 (へ　 ) 　　　ﾗﾝﾀ ﾀﾝﾀ
　 　 　 　 　　　　 >　　　　ﾀﾝ
0227１３２人目の素数さん
垢版 |
2022/05/02(月) 10:30:03.66ID:DYgxe9pf
　　　| ＼
　　　|Д｀)　ﾀﾞﾚﾓｲﾅｲ･･ｵﾄﾞﾙﾅﾗ ｲﾏﾉｳﾁ
　　　|⊂
　　　|


　　　　　♪　　Å
　　　♪　　　／ ＼　　　ﾗﾝﾀ ﾀﾝ
　　　　　　ヽ(´Д｀;)ﾉ 　　ﾗﾝﾀ ﾀﾝ
　　 　 　　　 (　 へ) 　　　ﾗﾝﾀ ﾗﾝﾀ
　 　 　 　 　　く 　　　　　　ﾀﾝ



　　　♪　　　　Å
　　　　　♪　／ ＼　　　ﾗﾝﾀ ﾗﾝﾀ
　　　　　　ヽ（;´Д｀）ﾉ　　ﾗﾝﾀ ﾀﾝ
　　 　 　　　 (へ　 ) 　　　ﾗﾝﾀ ﾀﾝﾀ
　 　 　 　 　　　　 >　　　　ﾀﾝ
0229１３２人目の素数さん
垢版 |
2022/12/22(木) 04:01:55.01ID:o2STx9rz
ゲーデルの不完全性定理の証明とか、

選択公理が命題として他の公理とは独立であることの証明とかできるかな？

もっと素朴に、√2が有理数では無いことの証明とか、
eやπが有理数ではないことの証明とか、
複素数係数の代数方程式は複素数の根を必ず持つことの証明とか。。。
0231１３２人目の素数さん
垢版 |
2022/12/22(木) 08:49:17.37ID:XxbM8r76
このようなソフトウェアに興味があるのですが、使えるようになるには、「証明論」のような本を
勉強しないとだめですよね。
0232１３２人目の素数さん
垢版 |
2022/12/22(木) 09:04:01.71ID:cem5kJiD
>>231
数学の知識よりも、プログラミングの知識のほうが重要だと思う。
関数型言語についてとか。
0233１３２人目の素数さん
垢版 |
2022/12/22(木) 11:50:58.34ID:5XpbsjKj
>>229
>ゲーデルの不完全性定理の証明
無矛盾(矛盾が証明されない)ならば
無矛盾性が証明されない、と読むから
神秘性や難しさを感じる

矛盾が証明されると矛盾する、という証明から
矛盾の証明が出来る、と読めばただのトリック
0234１３２人目の素数さん
垢版 |
2022/12/22(木) 11:55:35.37ID:5XpbsjKj
>>231
初心者は必ず騙されるが
証明論とは命題の証明方法の理論ではない

ちなみに命題の証明方法は別に難しくない
ただ証明がない場合、止まらないので
「アルゴリズム」とは言えないが
0235１３２人目の素数さん
垢版 |
2022/12/22(木) 21:53:35.10ID:cEUYFyKL
>>229
> √2が有理数では無いことの証明

Coqと同様の定理証明支援系であるHOL LightのTutorialに
11.1 Irrationality of √2がある
www.cl.cam.ac.uk/~jrh13/hol-light

実際にそこで証明しているのは
∀p,q. p×p=2×q×q ⇒ q=0 だけど
0237１３２人目の素数さん
垢版 |
2022/12/23(金) 21:32:30.54ID:hmYygAkB
証明が存在する命題は、有限回の操作によって必ず証明にたどり着く方法はある。
ただし、その有限回なる回数が一体どのぐらいの有限なのかだ。宇宙が終わるまで
かけても終わらない程の大きな回数であっても有限だから。
0238１３２人目の素数さん
垢版 |
2023/01/01(日) 23:05:56.42ID:bVpk4vzc
ある命題の成立に対して正しい証明が得られたならば、
その証明が正しいことを確認する作業は、必ず証明の
記述の長さの多項式オーダーの手間で可能なのだろうか？
0240１３２人目の素数さん
垢版 |
2023/01/02(月) 10:48:55.13ID:Tjm8RrUz
（Coqのような）証明系は正しい証明を記述したならば、それが正しいことを
必ず有限の時間で検証を終えて停止するのだろうか？
その有限の時間だといっても途方も無く長くなったりしないのだろうか？　
検証を行う前に、証明の記述に応じてそれに対する検証時間の上界が
事前に得られるものだろうか？
それともそのような上界は一般にはなくて、ただただ結果が出るまで
ずーっと待って運良く生きているうちに終わることを期せねばならないのだろうか？

C言語とかAlgolのような普通のプログラミング言語は、
コンパイルすべきプログラムの長さNに対するコンパイル完了までの時間は
O（N log N)程度になってる。もしもコンパイルの時間がたとえばO(N^2)
かかるような言語とかコンパイラであると、プログラムの記述が大規模になれば
実用性が低くて使い物にならない感じになる。
0241１３２人目の素数さん
垢版 |
2023/01/02(月) 11:14:46.62ID:bB/h5A70
>>240
証明になっているか否かのチェックは有限時間で可能

証明になってないギャップについて
ギャップが埋められるかどうかは
命題が証明できるかどうかと同じなので
有限時間では判定できない
0242１３２人目の素数さん
垢版 |
2023/01/02(月) 11:59:40.21ID:Tjm8RrUz
「証明」の長さがNであるときに、検証にかかる計算量がNについてあまり急増化
しないのであれば、検証システムは使い物になるが、Nについてたとえば多項式
オーダーではなかったならば、少しばかり長い「証明」を検証しようとすれば
現実的には「いつまでたっても終わらないなぁsigh、修論が落ちるな」、
ということになりそうだけれども、そのあたりはどうなっているのでしょうか？
0243１３２人目の素数さん
垢版 |
2023/01/02(月) 12:03:04.48ID:Tjm8RrUz
検証系が進歩した未来において、

　著者は自分の証明を検証系にかけて、
検証系に与えたソースコードも併せて提出する。
　論文の査読者はそのソースコードが正しく論文の定理や命題を表していることを
（ああたいへんだ）チェックして（そこが間違ってたらどうする？）、
検証系にかけて、正しく証明されることを確認したら、アクセプトする。

そうなったらとても面倒。論文のLaTeXのソースを提出するのとは次元が違う。
0244１３２人目の素数さん
垢版 |
2023/01/03(火) 02:56:16.38ID:EWDc62a3
ABC予想の証明の検証に時間がかかっていたようだけど、
Coqで検証すればよかったんじゃないの？できないの？
0245１３２人目の素数さん
垢版 |
2023/01/03(火) 04:56:18.54ID:JnLpt9Qh
人間の書いた人間に理解できるように書かれた証明を、
いろいろな前提知識の無い無垢のソフトに全く隙のない形で
完璧に記号だけを使って記述し直すというのは、とても大変な
作業になるだろう。暗黙知、専門家の常識、そういうものを総動員して
それらも含めて検証にかけなければ、論理が飛んでいることになるから
だろう。
0246１３２人目の素数さん
垢版 |
2023/01/03(火) 13:33:16.33ID:EWDc62a3
ABC予想の証明に否定的な数学者もいるようですから、
白黒はっきりつけるためにはした方が良さそうですね
おそろしく時間とお金（人件費）が掛かりそうですが…
0247１３２人目の素数さん
垢版 |
2023/01/03(火) 13:35:59.35ID:EWDc62a3
今まで正しいと思われていた定理がCoqで検証をしたら証明が間違っていて実は成立していなかった
という場合はあり得るのだろうか？
0248１３２人目の素数さん
垢版 |
2023/01/03(火) 21:49:08.81ID:JnLpt9Qh
定理をみな洗濯して候。選択公理を密輸入してたりとか。
0249１３２人目の素数さん
垢版 |
2023/01/05(木) 07:12:53.60ID:YJDwUIlt
基本的な質問で申し訳ありませんが、任意の数学の定理の証明は
その証明が正しいならばコンピューターが理解できる形の形式的な証明に書き直せますよね？
■ このスレッドは過去ログ倉庫に格納されています