- What is a proof of classical first-order logic?
- When are two proofs the same?
Π
_{1}≃ Π_{2} - Is there an intrinsic (non-syntactic?) representation?
Π
_{1}≃ Π_{2}*iff*Rep(Π_{1}) = Rep(Π_{2}) -
Representations should constitute a standalone proof system:
- Sound and complete
- Verifiable in polynomial time

- What are the benefits? Proof search (e.g. theorem proving)? Computation (e.g. cut elimination)?

- Proofs without syntax. Annals of Mathematics 143(3), 1065-1076, 2006.
- Towards Hilbert's 24th Problem. ENTCS 165, 2006.
- Intuitionistic proofs without syntax. With Willem Heijtjes and Lutz Straßburger. LICS 2019.
- First-order proofs without syntax, arXiv.org, June 2019.