このようなコードをLean Proverで検査しようとすると、補題test2でエラーが出る。1 gist.github.com いくら考えても原因がわからなかったのでGitHubのレポジトリにバグとして報告したところ、バグではなく仕様である、という返答を頂いた。 github.com ここ…

最近Lean Prover (Lean 3)で原始再帰的関数について証明を書いているので、それによって得られた知見を一つ紹介する。 gist.github.com inaccessible termとは何か ".(項)"の形のパターンはinaccesible termと呼ばれ、パターンマッチを行う際に、この部分は…

問題: No.551 夏休みの思い出（２） - yukicoder想定解は https://yukicoder.me/problems/no/551/editorial だが、原始根を無視してmod_sqrtを使って解いた。 mod_sqrtは(多分)O(log(p)^2)-timeで解けると思う。 gist.github.com

Rustでtreapと2-3 treeを実装してブログを書きました。treap: Treap on Rust - Codeforces2-3 tree: 2-3 tree on Rust - Codeforces(Codeforcesなので英語です)

Hackerrankの Indeed Machine Learning CodeSprintに参加しました。SVMで分類しようと試みましたが、結果は芳しくありませんでした。(175.33/1000点！w) この得点は、最初すべてのrowに対して"2-4-years-experience-needed"を返す実装を投げたことによって達…

tl;dr: Apacheで数独サーバーを作った話 - koba-e964の日記の続きです。 きっかけ 前回(Apacheで数独サーバーを作った話 - koba-e964の日記)の制作途中でいただいた以下のようなコメントがきっかけで、lighttpdでも作ってみることにしました。@kobae964 ligh…

tl;dr: Apache + Dockerでサーバーを作ってherokuにdeployしました。ソルバーは https://sparkle-sudoku-solver.herokuapp.com/ にあります。 作ったもの 数独パズルを解く、Web上で動くソルバーを作りました。(https://sparkle-sudoku-solver.herokuapp.com…