日記です。 リポジトリ: LayerXcom/cbc-casper-proof 概要 (私は LayerX の人ではないですが)LayerX 社の人と色々あって CBC Casper というブロックチェーンのプロトコルの検証作業を行いました。(主に定理証明士としてのお手伝い) 半年くらいかかったけどやりたかった証明についにたどり着いたよという話。 CBC Casper って何 わからん。(無知) 何かブロックチェーンのプロトコルの名前らしい。Ethereum 財団が目をつけてるらしい。いわゆるビットコインとは違ってブロックを頑張ってマシンをぶん回してマイニングしたりしないらしい(ビットコインは PoW で CBC Casper は PoS)。 詳しいことは詳しい人に聞いたほうがいいよ(真理)。 cf: CBC Casper と形式的検証 Isabelle で検証って何するの ブロックチェー
定理証明、特に定理証明支援系(Proof Assistant)はその存在こそ少しずつ浸透しつつあるような気がしないでもないけれど資料とか全然まとまってないのが不便だなと前々から思っていたのでリソースをまとめておきます。 これも追加してほしいみたいなのあったら教えてください。 Proof Assistants 始めるなら次の中から選ぶのがよいと思います。 Coq Calculus of constructionsベースの型システムとリッチなコマンドを備えた言語 このリストの中では最もコミュニティが大きい、入門書等も豊富 型システムと項を書くためのGallina, コンパイラへの命令を記述するためのVernacular, タクティクスの定義に使うLtacなどの言語が混ざって出てくるのが初心者には混乱必至 結構複雑な言語なので使いこなすのはそれなりに大変 Agda Martin-Löf type
これは一人Computer Scienceアドベントカレンダー 1日目の記事です。 概要的なもの 「一人アドベントカレンダーって面白そうだな、やってみたい」みたいなノリで登録したんですが、 25日毎日記事を同じテーマで投稿し続けるのどう考えてもめっちゃ大変なのでやはりここは自分が一番得意な分野で行くしかないかなとなりCS関係ということになりました。 上のQiitaのページでも書いてますが、キーワードとして"ラムダ計算・定理証明・Haskell・ML・圏論 とかなんかそのへん"を挙げていますので そのへんのお話になります。今のところは無難に定理証明を中心にテーマをいくつか選んでおいたので多分そのへんの話です。 スケジュール 最終的にはQiitaのカレンダー見ればわかることなんでいいんですが一応今後どういう感じで進めていくのかのスケジュール的なものをまとめておきます。 Isabelle編 Is
昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より： PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか？
400年の難問、｢ケプラー予想の証明｣やっと100％終わる2014.08.13 22:0021,548 satomi コペルニクスが提唱した地動説を、天体運行法則で不動のものにした偉人ヨハネス・ケプラー。 そのケプラーが1611年に提唱した｢球は、八百屋に山盛りのオレンジみたいにピラミッド型に並べると一番沢山入る｣という説が、400年の歳月を経て、100％正しかったことがコンピュータの力で証明されました。 この立体最密充填の解答は、誰でも直感的になんとなく正しいことがわかります。けれども証明するとなると超厄介で、世界歴代の天才がいくら頭脳を結集しても証明できなくて、ずっと｢定理｣ではなく｢ケプラー予想｣と呼ばれ続けてきた難題中の難題です（参考）。 証明したのは、米ピッツバーグ大学のトマス・ヘールズ教授です。もともと氏が1998年に発表し、｢フェルマーの最終定理以来の難問が解けた！｣と世界中
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
