[일반] 비둘기집 증명도 어렵구나 ...

[더블초코냥(218.232)]

Coq 얘가 엄밀하게 증명하는 법을 가르쳐줘서, 혼나면서 배우고 있음.

비둘기집 증명도 애먹고 있음.

정해진 도구만 가지고 논리를 전개하는 게 재밌는 사람에게 추천함.

[더블초코냥(218.232)]

그냥 내가 빠가인 듯 ㅋㅎㅎ

[익명(39.119)]

이딴 언어를 대체 누가쓰는거지

[익명(182.227)]

컴공에 허충길교수님이 활발하게 연구함

[익명(39.119)]

무시무시하구만

[더블초코냥(218.232)]

풀었다 ㅇㅅㅇ

[더블초코냥(218.232)]

https://gist.github.com/KiJeong-Lim/b793753c2b544ab4fff7656a766f3050

[익명(211.178)]

외국인이셨군요

[ScARfaCE(kayuaao)]

말그대로 컴퓨터한테 수학적 증명을 시키는거임?? 그럼 저거 말고도 또 뭐가 가능함?

[더블초코냥(218.232)]

증명 확인해 주는 거임. 주어진 규칙 밖에 못 쓰고, 컴퓨터는 올바르게 규칙 적용했는지 검사함.

[더블초코냥(218.232)]

Coq로 증명된 정리 중에는 4색정리가 유명함.

[ScARfaCE(kayuaao)]

확인해주는것만 해도 쩌는거같은데 ㅗㅜㅑ;;

[익명(182.227)]

4색정리를 CoQ으로 다시 검증한거지 애초에 쿽으로 증명한건 아니야

[익명(117.111)]

그 허충길 교수님 이번 학기에 뭐 가르치더라 시스템 프로그래밍인가

[익명(182.227)]

시프는 이강웅교수님이 가르치심

[성적표보여줘(2giyoung)]

오 신기하네