今日は確定申告をオンラインで済ませました。去年のデータを読み込ませて、それをもとに作成するので主な項目は記入済みで金額などを修正するだけで終わります。毎年やっていますが便利です。昔は税務署にでかけていって担当員の方に教えてもらいながら申告書を作成して書面で提出していました。コンピュータの発達で便利な世の中になりました。
今日は3月14日で円周率の日ですね。Google検索のサイトも円周率にちなむアニメーションにかわっていました。
円周率の日の今日3月14日はアインシュタインの誕生日で、ホーキングの命日だそうです。こちらをご覧ください。
https://www.todayinsci.com/3/3_14.htm
YouTubeにもこんな動画がありました。Happy π Dayの動画です。
Happy π Day from Leonardo de Moura: Formal Proofs, Lean, and the Future of Math
https://youtu.be/WXjY3HbPE9w
これは数学の証明を行うシステムLeanの開発者へのインタビューです。LEANはコンピュータによる形式証明システムとしてとみに有名です。京都大学の望月先生もABC予想の証明をLEANを使ってだれにも文句がつけられないように書き直す作業をはじめておられるようです。望月先生のブログ記事をどうぞ。
『Leanによる形式化は、長期的な検証や説明責任を可能にする記録装置となり得るか？』
https://plaza.rakuten.co.jp/shinichi0329/diary/202601010001/
私もABC予想の証明にLEANをつかってはどうかと妄想していると記事に書いたことがあります。LEANについても書いていますので埋め込んでおきます。
もうすぐLEANについての科学ジャーナリストによる本もでるそうです。面白そうですね。
The Proof in the Code
By Kevin Hartnett
https://www.quantabooks.org/books/the-proof-in-the-code/