Lean Hammer and TPTP

Stream: general

[Bas Spitters]

This paper introduces an extensional dependently typed HOL, as a standard for ATP. It's part of the TPTP family. It can be interpreted in PVS/F*, but not in Lean/Rocq.
It would be interesting to see whether a similar (intensional) standard could be derived from Lean Hammer (and perhaps Rocq hammer).
https://arxiv.org/pdf/2507.03208