Logic & proof complexity
When does one counting principle imply another?
My work on modular counting characterises implications between counting principles through the prime factors of their moduli.
Counting and the complexity of proofs →Logic · Information · Learning
Søren Riis
Reader in Computer Science · School of EECS
I study how mathematical structure shapes what systems can prove, communicate, decide, and learn.
My research connects mathematical logic and combinatorics with information flow, collective choice, and learning in games.
Featured · Interactive theory paper
The paper, unfolded
One Unit Separates Polynomial Time from Undecidability in Term Coding
Read the complete paper, select a paragraph to open its explanation, and follow the argument into exact Lean statements and proof steps.
- Read the mathematics
The entire typeset paper, from the first example to the final discussion.
- Follow the explanation
Open a paragraph to unpack its definitions, claims and connections.
- Inspect the formal proof
See exact hypotheses, Lean source, recorded goals and dependencies.
Unfold the paperClose the interactive paper
The interactive edition loads from GitHub Pages and needs an internet connection. If it does not appear, use the new-tab link or the PDF above.
The interactive edition distinguishes formal proofs, authored explanations and external assumptions.
Featured · Interactive theory paper
Learning in impartial games
Overcoming a Learning Bottleneck in Impartial Games: A Circuit Complexity Approach
Why can neural networks struggle with a game that has a simple, efficient solution? Using NIM, this paper identifies a representational bottleneck and develops three ways around it. Read the paper, explore the explanations, and follow the mathematical claims into their Lean formalisation.
Research
Questions, results & context →Information flow
What can a network infer from local information?
Graph guessing games connect local constraints with network coding. With Maximilien Gadouleau, I developed constructions linking guessing graphs, graph entropy, and communication.
Guessing numbers and network coding →Collective choice
How large can a Condorcet domain be?
For eight alternatives, the maximum is 224 orders, with a unique example up to isomorphism: a result with Charles Leedham-Green and Klas Markström.
The structure of collective preferences →Condorcet data: seven alternatives →
Explore the census and examples from our joint classification.
Games & learning
Does winning reveal understanding?
With Bei Zhou, I use impartial games to examine the gap between competitive performance and broader mastery in reinforcement learning.
Learning the structure of a game →Play Gomulda · 5 × 5 →
A game of maps, colour and strategy, invented by Cristoffer Crone. This was the board we most often played on in the Danish Gomulda Laug.
Try it →
Four guided research games, six deeper tools, and Gomulda.
Watch it →
Research explanations, recorded talks, and slides.
Read it →
The full bibliography, hosted PDFs, and earlier versions.
Selected publications
All papers and PDFs →Current research & preprints
Research context →Recent work on a one-unit complexity gap, text ecosystems, waiting-time paradoxes, and an entropic approach to extremal combinatorics.
Teaching
Logic, discrete structures, complexity, and computation at Queen Mary.
Box proofs: Fitch-style natural deduction
I developed this interactive teaching app to help students learn Fitch-style natural deduction in propositional logic. Build and check box proofs with practice exercises, hints, and step-by-step guidance.
Logic Lab: 2SAT and resolution
I developed this interactive teaching app for ECS651U: Computability, Complexity and Algorithms. Explore the 2SAT algorithm through implication graphs, and build and check resolution proofs.
Contact
s.riis@qmul.ac.uk
School of Electronic Engineering and Computer Science
Queen Mary University of London
Mile End Road, London E1 4NS