TPPMark 2025

This is a repository for submitted solutions to the TPPMark 2025 problem. See tppmark25.pdf for the problem description. Each submission is located under the directory named after the person who submitted it. All copyrights for all submissions belong to the respective authors.

Solutions (in the order of earliest submission)

• by Kenta Inoue
  The script runs on Coq with mathcomp 1.14.0. See his explanatory article here.

• by Makoto Kanazawa
  The script runs on Agda.

• by Hidekazu Segawa
  The script runs on Lean. The latest version is found here.

• by Akira Tanaka
  The script runs on Rocq 9.0.0 with MathComp. See memo.txt for the detail.

• by Ginga Hayakawa
  The script runs on Coq 8.16.0 with MathComp 2.0.0.

• by Jacques Garrigue
  The script runs on Rocq 9.0.0 with MathComp 2.4.

• by Masaya Taniguchi
  The script runs on Lean4. His solution written in Japanese is found here.

Prepared solution by the problem setter

• by Keisuke Nakano
  The script runs on Rocq 9.0.0 with MathComp 2.4.0.

Informal solution with LLM

• by miko
  The document describes a solution by Miko with Gemini 3 Pro.