- 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. Logic in Computer Science, 2019. With Willem Heijltjes and Lutz Straßburger.
- First-order proofs without syntax. ArXiv.org, June 2019.
- Combinatorial Proofs and Decomposition Theorems for First-order Logic. Logic in Computer Science, 2021. With Lutz Straßburger and Jui-Hsuan Wu