Statistical Notes🔗

Who am I? I'm an Assistant Professor of Statistics/Computer Science at the American University of Paris. I'm also a fellow researcher at Évry University (Paris-Saclay University).

You can find my publications, teachings, and contact information on my personal website: charles.doffy.net.

Why this blog? In my papers, I always use several mathematical lemmas whose proofs are often tedious and lengthy, far longer than their relative importance in the story I'm trying to tell. I'm a worrier, so I generally give the full proof, and it takes up a lot of pages and mental energy.

What's inside this blog? Building on recent advances in mathematical formalization, I will collect lemmas formalized in Lean 4 using Mathlib in this blog. This blog should be considered a work in progress, as results can be extended (weaker assumptions, stronger conclusions) or proofs rewritten (factorized or shortened) at a later date. Nevertheless, I will only present fully proved lemmas, with references to the relevant articles.

LLM use. Everything meant to be read by a fellow human being is generated by my own chaotic brain. I choose the topics I'm interested in and give lemmas I actually use.

I do rely on LLMs for

• maintaining the website (debugging, documenting the rendering process);

• get out of the weeds for certain Lean proofs. Lean's learning curve is steep; this is a crutch I allow myself. However, I rely less and less on LLMs as I go, and I read and try to simplify every bit of Lean code before I publish it.

Organization. The entries are in the order in which I publish them.