略歴
| 1988年3月 |
上智大学 理工学部 数学科卒業 |
| 1988年4月 |
エッソ石油株式会社 情報システム部 |
| 1991年 |
オーストリア共和国ヨハネス・ケプラー大学に留学 |
| 2000年9月 |
エクソンモービルジャパン合同会社 情報システム部 |
| 2006年9月 |
信州大学大学院 工学研究科 情報工学専攻 修士課程 修了 |
| 2010年9月 |
信州大学大学院 総合工学系研究科 システム開発工学専攻 博士課程 修了 |
| 2012年5月 |
株式会社東燃ゼネラル石油 情報システム部 |
| 2017年4月 |
株式会社JXTGエネルギー（現 ENEOS）情報システム部 |
| 2021年4月 |
立正大学 データサイエンス学部・文学部 非常勤講師 |
| 2025年4月 |
現職 |
研究テーマ
形式化数学とは、数学の理論や定理をコンピュータで扱えるようにコードとして表し、厳密な論理と推論規則にもとづいて再構成することを指します。こうして形式化された定理を蓄積した「ライブラリ」を活用することで、新しい定理の検証も可能になります。
定理証明支援系（ITP：Interactive Theorem Prover）は、その定理をコード化する際に用いるソフトウェアであります。ITPを使うことで、定理やアルゴリズム、暗号の安全性などの正しさを厳密に検証することができます。さまざまな対象を正しく検証するには、ライブラリの整備が重要であり、これは大切な研究テーマです。
さらに、数学教育の面でも、証明を形式化していく過程を通じて、「なぜその証明が正しいのか」を深く理解できるようになり、学習者にとって「なるほど！」と腑に落ちる理解につながるのではと考え、こうした形式化の教育への応用についてもテーマにしています。
担当科目、ゼミ
微積分学及び同演習, 線型代数及び同演習, 応用数学, データサイエンティストの世界, ゼミI, ゼミII.
教員から学生へのメッセージ
「自分はどんな人間になりたいのか？」
そんな大きなビジョンを、ぜひ考えてみてください。これは、私自身が学生時代にアドバイスしてもらいたかったことの一つです。
なぜなら、大きなビジョンを持っていれば、小さな目標でつまずいてもあまり落ち込まずにすみ、再びそのビジョンに向かって歩みを進めることができるからです。
数学の学習におけるアドバイスとして、問題を解いたり数学の文章を読んだりして、よくわからないことがあれば、紙と鉛筆を使って図を描いたり、簡単な例を計算してみることをおすすめします。
あきらめずに問題と向き合い続けることで、少しずつ理解が深まってくるものです。疑問があれば、自分の手で図を描いたり、計算して観察することが大切です。
こうした取り組みは、“サイエンス脳”を育てるトレーニングにもなります。ぜひ前向きに取り組んでみてください。
研究業績等
1) Yasushige Watase, Introduction to Algebraic Geometry, Formalized Mathematics, Vol. 31, No. 1, pp. 67–73, October 2023, Sciendo.
2) Yasushige Watase, Embedding Principle for Rings and Abelian Groups, Formalized Mathematics, Vol. 31, No. 1, pp. 143–150, December 2023, Sciendo.
3) Yasushige Watase, Formal Proof of Transcendence of the Number e. Part I, Formalized Mathematics, Vol. 32, No. 1, pp. 111–120, December 2024, Sciendo.
4) Yasushige Watase, Formal Proof of Transcendence of the Number e. Part II, Formalized Mathematics, Vol. 32, No. 1, pp. 121–131, December 2024, Sciendo.
5) 渡瀬泰成, 「データサイエンス学部に於ける数学教育と形式化数学の活用 — 定理証明支援系と大規模言語モデルを活用した数学教育の可能性」, 国際ICT利用研究学会研究会研究論文誌, 第4巻第1号, pp. 11–15, 2025年.
所属学会
日本Mizar、国際ICT利用研究学会、日本数学会
