Welcome

Welcome. This is the first post on my research blog. I’ll use it for expository notes, internship updates, and rough thoughts on the things I work on.

What I work on

I’m a 4th-year computer science student at the ENS de Lyon. The questions that pull me in sit at the intersection of logic and computer science: type theory, constructive mathematics, computability, and the kind of proofs you can actually run inside a proof assistant.

A few recurring topics:

• Algorithmic randomness. What does it mean for an infinite sequence to be “random”? Algorithmic randomness pins this down using computability and measure theory: a sequence is random if no algorithm can predict or compress it.
• Synthetic and constructive foundations. Doing analysis, topology, or randomness inside a constructive setting where every existence proof comes with a procedure. Currently a big part of my Inria internship.
• Formalisation. Proof assistants like Rocq and Agda. Type-theoretic foundations and what changes when you actually have to write the proofs down.
• Reverse mathematics. Working out which axioms a theorem really needs, instead of which ones are convenient.

A small example

A flavor of the kind of question I find irresistible: are the digits of $\pi$ random?

Number theory has a precise version of this question. A real number $x$ is normal in base $b$ if every finite string of digits appears in its base-$b$ expansion with the expected asymptotic frequency. In base 10, that means each digit $0, 1, \ldots, 9$ appears with frequency $1/10$, each pair $00, 01, \ldots, 99$ with frequency $1/100$, and so on.

Despite overwhelming numerical evidence, whether $\pi$, $e$, or $\sqrt{2}$ is normal in any base is still open. Nobody knows.

Algorithmic randomness gives a stronger notion: a sequence is Martin-Löf random if no computable test can detect a pattern in it. By that definition, $\pi$ definitely isn’t random, since the digits are computable. But a lot of the structure people would intuitively call “randomness” is captured exactly there, and constructively reformulating those notions is what I’ve been working on.

More to come.