Proof Theory & Automation

Overview

Proof theory studies the structure of mathematical proofs themselves. My work in this area focuses on structural proof theory for substructural logics — particularly linear and intuitionistic logic — and on leveraging these insights to build better automation for interactive theorem provers.

Structural Proof Theory

Skolemization for intuitionistic linear logic. Classical Skolemization replaces existential quantifiers with function symbols, enabling efficient automated reasoning. Extending this to intuitionistic and linear settings requires care, because the structural rules that classical logic takes for granted are absent. I have developed Skolemization techniques for intuitionistic linear logic, opening the door to more efficient proof search in resource-sensitive logics.

Session types and linear logic. Linear logic provides a natural framework for reasoning about protocols and concurrent systems. I have contributed to the study of session types as a bridge between linear logic and practical programming language constructs.

AI-Assisted Theorem Proving

I am increasingly interested in the intersection of large language models and interactive theorem proving:

• Automated proof generation — prompting and fine-tuning LLMs to produce proofs that are verified end-to-end by the Rocq kernel.
• Proof translation — automatically translating proofs between different proof assistants (e.g., Lean to Rocq).
• Learning environments — AI-assisted tools that guide students through interactive theorem proving with hints and feedback.

Selected Publications

1. Alessandro Bruni, Eike Ritter, Carsten Schürmann: Skolemization for Intuitionistic Linear Logic. IJCAR 2024 arXiv

2. Peter Brottveit Bock, Alessandro Bruni, Agata Murawska and Carsten Schürmann: Representing Session Types. Dale Miller’s Festschrift, 2016