おはようございます．

2本目の記事が新年のご挨拶というのもいかがなものかとは思いますが，年末にかけて Stanley Burris, H. P. Sankappanavar "A Course in Universal Algebra" の Lean による形式検証(WIP)に取り組んでいてブログの更新がおろそかになっていました．

昨年は手出しできる領域を飛躍的に広げることのできた一年でしたが，一方で方向性を絞り切れずにだらだらと色々なものに手を出してしまっていたことも否めないため，本年はしっかり一本の筋を通して成果を上げられるようにしていきたいところです． 具体的には修士論文と就活が控えているため，色々と絞っていきたい所存です．

こちらのサイトも色々拡充してポートフォリオらしい感じにしていきたいですね． ひとまず現状数式入りのマークダウンが Earmark(elixir の markdown-to-HTML ライブラリ)で上手く処理できない問題があるので，なんとかして数学の記事を書ける状態まで持っていきたいです． どちらにせよ，こういうのは読み込み側は素の HTML を読み込むようにして，読み込ませる HTML を諸ツールの HTML 出力で用意するのが柔軟で良いということは分かってきました．

あと今年は F# や Lean のコミュニティを積極的に盛り上げていきたい気持ちがあります． 特に F#，コミュニティが悲惨な状況で悲しすぎるのでなんとかしたい． やっぱり F# はこんな軽薄な扱いをされていい言語ではないです．

それから Lean も今の勢いをさらに押し上げて活気づけていきたいところです． もくもく会とかやってみたいのでだれか影響力ある人呼びかけお願いします(他力本願)．

そんな感じで本年も慎ましく頑張りたいと思います．