このエントリーをはてなブックマークに追加

Aug

22

第102回 ProofCafe

名古屋Coq勉強会

Registration info

Description

萩原、アフェルト 著 「Coq/SSReflect/MathCompによる定理証明」森北出版 の4章を読んでいきます。

4.6 bigop.v

参加をご希望のかたは、管理者までお問い合わせください。


Coq/MathComp をセットアップしたのち、

https://github.com/suharahiromichi/coq/blob/master/csm/csm_4_6_bigop.v

をダウンロードしておいてください。 資料は改訂していますから、申し訳ありまあせんが、開始直前に再度ダウンロードしなおしてください。

また、https://github.com/suharahiromichi/coq/blob/master/common/ssromega.v もダウンロードして同じディレクトリに置き coqc ssromega.v を実行して、ssromega.vo ができていることを確認してください。


問題 1.

任意のnについて、以下が成り立つことを証明してください。

2 * (\sum_(0 <= x < n.+1) x) = n * n.+1

6 * (\sum_(0 <= x < n.+1) x^2) = n * n.+1 * n.*2.+1

問題 2.

自然数 n が合成数なら、2^n - 1 も合成数であることを証明してください。

解答は説明のなかでおこないます。

以上

Feed

SUHARA Hiromichi

SUHARA Hiromichiさんが資料をアップしました。

08/22/2020 10:47

SUHARA Hiromichi

SUHARA Hiromichiさんが資料をアップしました。

08/16/2020 17:22

SUHARA Hiromichi

SUHARA Hiromichiさんが資料をアップしました。

08/01/2020 08:00

SUHARA Hiromichi

SUHARA Hiromichi published 第102回 ProofCafe.

07/25/2020 18:18

第102回 PoofCafe を公開しました!

Group

ProofCafe

Number of events 52

Members 44

Ended

2020/08/22(Sat)

13:30
15:30

Registration Period
2020/07/25(Sat) 18:18 〜
2020/08/22(Sat) 15:30

Location

オンライン(skype)

オンライン(skype)