情報数理科学演習I

第1回 ガイダンス。対話型AIを利用した計算や証明の作成の仕方についても学ぶ。 第2回 形式証明支援系Lean 4の基礎 第3回 形式証明支援系Lean 4の実践 第4回 形式証明支援系Lean 4の応用 第5回 形式証明支援系Lean 4の発展 第6回 写像、2項関係と順序 第7回 LaTeX(担当松島) 第8回 束 第9回 集合の濃度 第10回 公理的集合論 第11回 距離空間 第12回 群とその準同型 第13回 環と体

授業の情報はUTOLに公開されるので、UTOLをチェックせよ。 問題を解くのが中心の回と、コンピュータの操作が中心の回がある。 問題を解く回では、まず授業でその日の題材について解説する。 履修者は出題された問題を主に授業中に解いて、チェックを受ける。 コンピュータを使う回では指示された操作を行いUTOLを通じて課題を提出することになる予定である。 この授業は情報数理科学Iの授業と連動しており、その授業を履修中であることを前提に進められる。 また、無線LANでインターネットに繋ぐことのできるノートパソコンを所持していることを前提に進められる。WindowsでもMacでも構わない。

毎回、提出する課題を評価する。

この授業は、広域システムコースの広域システム特論IIIとの両面開講である。広域システム特論IIIを別の年度で履修することは制度上可能だがその場合は履修を取り消す。