自己紹介
略歴
2010年 麻布学園麻布中学校入学
2013年 同校 卒業
麻布学園麻布高校 入学
2016年 同校 卒業
東京大学教養学部理科I類へ進学
2018年 東京大学理学部数学科へ進学
2019年 東大数学科Slackワークスペース立ち上げに参加
2020年 東京大学理学部数学科 卒業 (理学部学修奨励賞受賞)
東京大学大学院数理科学研究科修士課程(指導教員:新井 敏康先生)へ進学
FoPM学生Slackワークスペース立ち上げに参加
2022年 東京大学大学院数理科学研究科修士課程 修了(修士号取得、数理科学研究科長賞受賞)
同学科 博士課程(指導教員は引き続き新井 敏康先生)へ進学
「日本学術振興会特別研究員(DC1)」採用
「若手研究者海外挑戦プログラム」採用
2023年 Charles Universityにvisiting studentとして在籍
2024年 帰国。新井先生のご退職に伴って、指導教員が酒井 拓史 先生に変更
中心的な興味の変遷
※概略を述べるにとどめます。高校数学までを修めた方ならば読めて、かつなるべく短くなるよう、誤解のない範囲で捨象したこともあります。詳細について気になられる方は、直接お会いした際に是非お気軽にお尋ねください
※専門用語について、イメージをお求めの方は、まずは分野紹介をご覧ください。より詳しく学ばれたい方は、おすすめ閲覧コースProof Complexity入門を参照ください
中学2年生の頃のユークリッド幾何の授業で、「同一平面上の相異なる二円の共有点は高々2個である」ということを先生が厳密に証明しているのに心震えたのが、"数学との出会い"でした。
中学3年生の時、代入ができなくなりました。
「なるほど
『x=yならばf(x)=f(y)』、
その通りだと思うけど、でもそれ証明してなくない?」
と考えたからでした。この疑問を中高の先生方にぶつけたところ、とても真摯に対応してくださって、「これを読んでみたら?」と勧められたのが、数理論理学の教科書でした。これが、"数理論理学との出会い"でした(ちなみにその本では、上の"代入の原理"は「等号公理」と記載されていました。「公理ならば仕方がない」と納得した次第です)。
中学3年生から高校にかけて、数理論理学の勉強を試みましたが、すぐに挫折しました。数理論理学の勉強に必要な数学全般の基礎的な事項(「集合と位相」の内容など)を、押さえていなかったからです。結局高校では、この"基礎的な事項"に習熟することに時間を使うことになります。
しかし、この間に育った疑問は、権にとってとても重要でした。
「僕たちの論理は、なぜ正しいのだろう?例えば、
『AまたはBが成り立ち、さらにAは成り立たないならば、Bが成り立つ』。
やっぱりその通りだと思うけど、それに証明は要らないのだろうか?」
これはきっと数学の問いではないと思ったので、大学の教養課程では言語学や哲学、脳科学など、関連しそうな分野を見て回りました。そしてそのうちに、上の問いについては考えないことに決めました。
「僕たちは論理の正当性を前提に、経験的な事実をまとめ上げ、理解する生き物なのだ」
と思うようになったのです。
しかし、そのように立場を変えることで、新たに問いが生じました。
「僕たちはそういう(上のような)生き物だとして、では僕たちの論理には何ができて何ができないのだろう?」
この問いへのアプローチはさまざまに考えられましたが、権は数理論理学の観点から考察を進めていきたいと考えました。これが学部3年生の頃の話です。
その後、数理論理学の基礎的な事項を(改めて)勉強していき、その中で、Proof Complexityに出会い、運命を感じました。
「僕たちの論理の能力を、証明の長さという観点から分析することができたら面白い」
と思うようになりました。より具体的には、
「『一階述語論理 のもとでのZFC』などの"ポピュラーな"数学の(数学的対象としての)定式化のもと、具体的な定理(例えばグラフ理論の四色定理など)に、『最低でもいくらくらいの長さの証明が必要である』といった評価を与える仕事をしていきたい」
と考えました。 これは今でも権の究極的な目標になっています(この問題はとても魅力的に感じられます。与えられた数学理論Tのもと、主張αの証明・反証の長さをある程度でも見積もることができれば、場合によっては、αの証明・反証を行う前に、その証明・反証の難しさが測れるかもしれないわけです。極端な話、その長さが天文学的になると分かったなら、
「Tからαを証明・反証する」
という問題設定そのものについて、再考する必要が出てくるわけです。もちろん、
「どんなTやαにも通用する、正確で、かつコンピューターに実装可能な評価法は存在しない」(計算可能性理論におけるChurchの定理の簡単な応用です)
ことが知られていますが、興味深いTやαに対して、十分な精度の評価法が存在する可能性は残されていますし、この研究の過程で、モデル理論・計算複雑性理論・組み合わせ論に飛躍的な進歩がもたらされる可能性も、さまざまな研究結果から示唆されています)。
しかし、Proof Complexityの勉強を進める中で、
「僕たちは命題論理 の証明の長さすら、よく理解できていない」
ということを知りました。
そこで、まずは命題論理のproof complexityについて調べることに決め、修士課程ではその研究を主に行っていました。より具体的には、constant-depth Frege systemのproof complexityについて、どういった数え上げの基本法則(例えば鳩の巣原理など)の導出が短い長さで行えるか、という観点から分析をしました。
用語について直観的な説明を与えます:そもそも「証明の長さ」という量は、一般には証明系に依存します。ややもすれば、Proof Complexityは、"証明系に依存するアドホックな量"を調べる分野になってしまいますが、実際には、例えば
「証明する主張をどんどん長くしていった時の証明の長さの発展」
に着目することで、頑健で普遍的な数学的対象を得ることができ、権が調べていたのはこれです。
そして、数学を営む者にとって身近な(命題論理の)証明系の一つにFrege system があります。これは、数理論理学の教科書が数学的証明を定式化するならば必ず触れるであろうHilbert流証明系、自然演繹、シーケント計算と(p-equivalenceの意味で) "等価" な証明系です。
「Frege systemでの証明の長さを調べる」
問題は、Proof Complexityの最前線に位置し、とても自然な証明系を相手にしているために大変重要です。権が調べてきたconstant-depth Frege systemというのは、Frege systemを弱めて得られる証明系の中で、
「ある種の主張を証明するのに(主張の長さに対して)指数関数的に長い証明が必要である」
ということが知られている最強のもの です。つまり、既存の技術でギリギリ、証明の長さの(興味深い)下界(lower bound)が得られるところに着目して、証明の長さを解析する新たな知見を探ったり、新しい証明技術の開発を試みたりしていました。
成果については、権の修士論文をご覧ください。
現在は、博士課程にて、修士課程での研究をより精緻で強力なものにすることを試みています。