Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:11:34 JST きゅーけー

   これはいまどきの計算機なら、多倍長整数を使って簡単に求められてしまうな。Guile を使ってぱぱっと比較してしまった(数学しろ)。https://www.youtube.com/watch?v=BNa8eJqjB6I

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:13:57 JST きゅーけー

     in reply to

     Guile には 「こうかつ、ずるさ、悪知恵」という意味があるんでしゃあない(関係ない)。https://ejje.weblio.jp/content/guile

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:18:47 JST きゅーけー

     in reply to

     こんな感じでちゃっちゃっと求められてしまう(動画のネタバレ回避のため閲覧注意)。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:35:06 JST きゅーけー

     in reply to

     ACL2 でもやった(ただ計算によって比較しただけなので、この定理証明に ACL2 のうまみはない)。これを一般化したようなものを証明できたら凄そうだけど大変そうなのでやらない。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:36:23 JST きゅーけー

     in reply to

     動画をちゃんとみていけそうならやるか。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:37:53 JST きゅーけー

     in reply to

     この人 x^x 乗が好きでたまらない人なんかな。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:47:36 JST きゅーけー

     in reply to

     一般解を ACL2 で求めるのいけるかもしれないのでちょっとやってみるか。あんまり時間かかりそうなら諦めよう。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 16:04:12 JST きゅーけー

     in reply to

     これ arithmetic ライブラリに加えて補助定理を一個書くだけで証明できるかもという期待と、自分の考えている補助定理の証明にどれくらい時間がかかるかという不安がせめぎあっている。解けたらせっかくなので記事にしようかな。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 16:24:45 JST きゅーけー

     in reply to

     そんな簡単じゃないなこれ。あとで思いだしたときに再チャレンジしよう。