2024.07.20
https://gyazo.com/82caa0308f142d051338cd3d0cf7dec4
メモ
サイゼリヤで作業をしてみた.意外と進んだ.
思った
数学の証明は定理証明支援系で実装してgithubとかで公開するのが将来的にはスタンダードになるはず 理想的にはそうなってほしいが、過渡期であるということも踏まえてもこれがメジャーにはならなさそうな気はする.証明の形式化に伴う工数があまりにも大きくなり不要に時間を食ってしまう(人間的には「自明な」で済ませられる部分が形式化すると技術的に面倒なことが多々ある)
全てを形式化して検証したい私のような暇人がたくさん居れば良いが今後増えてくれるのかはわからない がんばって啓蒙しましょう
自然言語の証明から適当に形式化された証明を吐いてくれるLLMとかの開発はあり、それでどうにか効率的に実装を進めるとかの方向性はあると思う
やっている身からすると,証明の精緻化という面でミスが見つかりうるかもしれないが,全てに対してそれをやりたいかという暇人がやっぱりそんなに居ないのではないだろうかと言う気もする.
別件
あるんだろうか?
やった
要するにこれのことである
$ \vdash_\Lambda \Box A \implies \vdash_\Lambda A
$ \bf GLではこれが成り立つ.
ちょっとネ
思った
ロシデレの影響で普通にロシア語学んでみたすぎるになってる