最近ずっと Lean のことを考えています。
命題論理の真理値表を見ても「命題がみんな True か False のどちらかになるのは排中律という強い仮定をおいているからこそであって、それは本質じゃない気がするな～～」と思ってしまうようになりました。ZF に基づく数学をやっていたころには全然思わなかったことです。時の流れを感じますね。
さて、前回の振り返りは７月でした。
気が付けばもう９月です。そろそろ振り返り記事を書こうと思います。
Lean by Example に演習問題を記載するようになった
相変わらず Lean by Example の編集・執筆をメインに活動しているのですが、大きな変更としてリファレンスだけでなく「演習問題」を載せるようにしました。これは、主に以下のような狙いがあります：
Mathematics in Lean という Lean で数学をどのようにすれば実装できるかを解説する有名なチュートリアルがあるのですが、今までの Lean by Example には言語仕様のリファレンスしかなく、チュートリアルやガイド的な内容がありませんでした。演習問題を載せることにより、そういった内容を拾うことができるようになり、「All in One な Lean のドキュメントを作る」という究極目標に一歩近づけるなと考えました。
そもそも数学はパズルっぽいのですが、Lean を使うと完全にパズルゲームそのものになります。Natural Number Game (以下 NNG )という有名な Lean のチュートリアルがあるのですが、それはまさに「パズルゲームとして」基本的な自然数の性質をペアノの公理から示す過程を楽しむというものになっています。Lean by Example でも、Lean をパズルとして楽しむという体験を提供することで、読者に数学のおもしろさと Lean の楽しさを理解してもらいたいという気持ちがあります。
演習問題という対話的コンテンツを用意することで、配信者にもネタとして使ってもらえるようにする。
Lean by Example は「初心者である私が、勉強しながら学んだことを集積する場」という役割も果たしています。演習問題の登場により、いままで記載できなかったネタが記載できるようになり、ますます勉強がはかどりそう。
演習問題を介して、著者である私が数学を「Lean による演習問題化」という体験を通して再体験することができ、数学への理解を深めることができるかもしれない。
狙いがたくさんですね。上記のように「私にとって嬉しい」という側面が強いのですが、lean ja のサーバメンバーからも評判がわりと良くて良かったです。今後、ますます演習問題を充実させていきたいです。
Lean by Example のアクセス解析をするようになった
Google アナリティクスを使って、アクセス数を解析しはじめました。これにより、一日あたり 200 以上のアクセスを集められている（…で合ってるのか？）ことがわかりました。
またユーザ数も良い感じですね。
アクセス状況は今後重要な指標となると思うので、次回の振り返りでも書いていこうと思います。
