22nd Theorem Proving and Provers Meeting

TPP is held every year since 2005, and provides a forum to exchange ideas for both users and implementors of theorem provers and proof assistants. We aim to make TPP a place where people interested in theorem proving technologies can gather widely.

Updates

  • October 3, 2026: Updated the invited talk information.
  • September 24, 2026: Published TPP-mark 2026.
  • September 1, 2026: Opened registration for participation and presentations.
  • July 5, 2026: Published the TPP 2026 website.

Event Information

  • Date: Monday, November 16, 2026 to Tuesday, November 17, 2026
  • Venue: RIKEN Center for Advanced Intelligence Project (RIKEN AIP), Tokyo Office
  • Address: 15F, Nihonbashi 1-chome Mitsui Building, 1-4-1 Nihonbashi, Chuo-ku, Tokyo 103-0027, Japan (Access information)
  • Co-host: RIKEN Center for Advanced Intelligence Project (RIKEN AIP)
  • Organizers: Sho Sonoda (RIKEN AIP / CyberAgent), Masaya Taniguchi (RIKEN AIP)
  • Contact: sho.sonoda@riken.jp

Invited Speakers

  • Dr. Mario Carneiro (University of Cambridge)

    Title: Metamath Zero: Trust All the Way Down

    Abstract

    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.

  • Prof. Daisuke Bekki (Ochanomizu University)

    Title: Propositions as Types, Meanings as Verification: Prop, Type, and Anaphora in Dependent Type Semantics

    Abstract

    In Lean, Prop is proof-irrelevant, and all true propositions are identified with True. This is an adequate design for the formalisation of mathematics, but its granularity is not adequate for a theory of meaning in natural language. This talk argues that natural language semantics needs Type rather than Prop.

    The first argument starts from the observation that truth-conditional semantics, the standard approach in the formal semantics of natural language, has exactly the granularity of Prop: the meaning of a proposition is the collection of models that make it true, and hence all tautologies have the same meaning. Its proof-theoretic alternative, verificationist semantics, takes the meaning of a proposition to be the collection of pairs of a context and a proof term that satisfy the typing judgment, and distinguishes different tautologies by their normal proof terms. Moreover, the capacity to understand a proposition, in Dummett’s sense, reduces to the decidability of type checking.

    The second argument concerns semantic composition for anaphora in natural language. In donkey sentences and E-type anaphora, a pronoun refers to a witness projected out of a proof term of a Sigma-type, which is exactly what existential quantification in Prop forbids. Dependent Type Semantics (DTS) is a theory of meaning that resolves these problems uniformly by introducing underspecified types. A pronoun is an open proof whose solution is found by proof search launched from inside type checking, and both anaphora resolution and presupposition projection reduce to proof search.

    The second half of the talk describes how this is implemented in lightblue (a CCG parser equipped with a bidirectional type checker for DTS) and wani (an automated theorem prover for the fragment of DTS with Pi-types, Sigma-types, enumeration types, equality types and disjoint union types), how distributional semantics stands in for axioms about the atomic predicates of DTS (Neural DTS), and the tension between natural language meaning and proof assistants: distinguishable witnesses, open proofs, and normal forms as the objects of meaning.

Participation and Presentation Registration

Deadline: October 31 (Sat)

https://forms.gle/yX8DjLX59LNquCJN9

TPP-mark

TPP-mark 2026: “Formalize the solved results for Othello in a proof assistant”

  • Problem author: Masaya Taniguchi
  • Deadline: The day before TPP 2026 (November 15, 2026)
  • Submit solutions to: {masaya.taniguchi, sho.sonoda} AT riken.jp

Past TPPs

Show past meeting pages

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

日本語版も用意しています。