22nd Theorem Proving and Provers Meeting

TPP は2005年から毎年開催される、定理証明器や証明支援系のユーザと開発者がアイデアを交換する場です。 定理証明技術に関心のある方々が広く集まる場を目指しています。

更新情報

  • 2026年10月3日： 招待講演情報を更新しました。
  • 2026年9月24日： TPP-mark 2026 を公開しました。
  • 2026年9月1日： 参加・発表の募集を開始しました。
  • 2026年7月5日： TPP 2026 のページを公開しました。

開催情報

  • 開催日程：2026年11月16日（月）から17日（火）まで
  • 会場：理化学研究所 革新知能統合研究センター（理研AIP）東京オフィス
  • 住所：〒103-0027 東京都中央区日本橋1-4-1 日本橋一丁目三井ビルディング15階（アクセス情報）
  • 共催：理化学研究所 革新知能統合研究センター（理研AIP）
  • 幹事：園田翔（理研AIP / CyberAgent）、谷口雅弥（理研AIP）
  • 連絡先：sho.sonoda@riken.jp

招待講演者

  • Dr. Mario Carneiro（University of Cambridge）

    講演タイトル： Metamath Zero: Trust All the Way Down

    概要

    When a theorem is “formally verified”, what exactly are we being asked to believe? Underneath the tactics there is an elaborator, underneath that a kernel, and underneath the kernel a runtime, a compiler, an operating system, and a chip. This year has made the question concrete: more than twenty soundness bugs were found in the Lean kernel, several by AI systems generating adversarial proof terms directly, and one of them briefly “disproved” the Collatz conjecture. The de Bruijn criterion (a small, independent checker re-checks everything) is a good design principle, but it is also an empirical claim about one particular program, and it deserves to be examined.

    This talk presents a research programme built around that question. Lean4Lean is a reimplementation of Lean’s kernel in Lean together with a formal specification of its type theory and an in-progress proof that the one meets the other; the proof has already found a kernel bug present since Lean 4.0. Metamath Zero (MM0) is the other end of the spectrum: a proof language designed so that the checker stays under 3,000 lines of C, has seven independent implementations, keeps the specification and the proof in separate files, and fixes no foundation of its own. Its goal theorem, stated and proved in MM0 itself, is that a particular x86-64 executable is a correct MM0 verifier, with the proof generated by a compiler for a separation-logic-typed systems language. I will show the languages and the browser tools, report on how far the bottom theorem has progressed, including how the x86 specification is tested against real hardware, and sketch what it would take to keep going below the instruction set, to the gates and the transistors.

  • 戸次大介 教授（お茶の水女子大学）

    タイトル： Propositions as Types, Meanings as Verification: Prop, Type, and Anaphora in Dependent Type Semantics

    概要

    Lean の Prop は proof irrelevant であり、すべての真な命題は True と同一視される。これは数学の形式化にとっては十分な設計であるが、自然言語の意味の理論にとっては十分な粒度とはいえない。つまり、自然言語の意味論には Prop ではなく Type が必要である、ということを論じる。

    第一の論点は、自然言語の形式意味論において標準的な真理条件的意味論が、まさに Prop と同じ粒度をもつという指摘にはじまる。すなわち命題の意味は、それを真にするモデルの集まりであり、したがってすべてのトートロジーは同じ意味をもつことになる。これに対する証明論的な代案である検証条件的意味論は、命題の意味を、型判断をみたす文脈と証明項の組の集まりとして与え、異なるトートロジーを正規証明項によって区別する。また、ダメットがいう命題を理解する能力は、型検査の決定可能性に帰着する。

    第二の論点として、自然言語における照応の意味合成の問題がある。ロバ文や E タイプ照応において、代名詞は Σ 型の証明項から射影された witness を指しており、これはまさに Prop における存在量化が禁じていることである。依存型意味論(DTS)は、未指定型を導入してこれらの問題を統一的に解消する意味理論である。代名詞は、型検査の内部から起動される証明探索によって解が求められる open proof であり、照応解決と前提投射はいずれも証明探索に帰着する。

    講演の後半では、これが lightblue（DTS の双方向型検査器を備えた CCG パーザ）と wani（Π 型・Σ 型・枚挙型・等式型・直和型をもつ DTS の断片のための自動定理証明器）に実装されていること、分散意味論が DTS の原子述語に関する公理を代替すること(Neural DTS)、そして自然言語の意味と証明支援系の間の緊張関係（すなわち、区別できる witness、open proof、意味の対象としての正規形）について述べる。

参加・発表登録

10月31日（土）締切

フォーム : https://forms.gle/yX8DjLX59LNquCJN9

会場の席数に限りがありますので、お早めの登録をおすすめします。

TPP-mark

TPP-mark 2026「Othello の解決結果を定理証明支援系で形式化せよ」

  • 作問：谷口雅弥（Masaya Taniguchi）
  • 締切：TPP2026前日（2026年11月15日）
  • 解答提出先：{masaya.taniguchi, sho.sonoda} AT riken.jp

これまでのTPP

過去の開催ページを表示する

TPP 2025 / TPP 2024 / TPP 2023 / TPP 2022 / TPP 2021 / TPP 2020 / TPP 2019 / TPP 2018 / TPP 2017 / TPP 2016 / TPP 2015 / TPP 2014 / TPP 2013 / TPP 2012 / TPP 2011 / TPP 2010 / TPP 2009 / TPP 2008 / TPP 2007 / TPP 2006 / TPP 2005

English version is also available.