Mathematical engineer. Deep interest formal methods. Below is a selection of projects, active and completed.

A Markdown-to-LaTeX parser, installable via pip install MarkdownToLaTeX.

The parser implements a state machine with bounded memory for context tracking. The design was formally specified in TLA+ before being implemented in Python — following the methodology described in Lamport's Specifying Systems.

• State machine source
• LaTeX document structuring
• Documentation

A new version of MarkdowntoLaTeX is currently under development. Switch to the dev branch to follow its progress.

• specifications

Selected solutions to Rudin's Functional Analysis. Ongoing revision and expansion. You can download them as a pdf file.

Formal specifications written in TLA+. Includes a specification of the reversible hoist invented by Renaissance architect Brunelleschi. (Historical reference)

A collection of SAT-style mathematics problems, written for teaching, with an appendix for advanced readers. Each exercise is accompanied by a Python program that computes the solution. Currently available in French; an English edition is in preparation.

An interactive job search interface that renders results on OpenStreetMap, backed by the Adzuna Jobs API.

Python3 translation of Bellingcat's open-source intelligence guides.

This parser counts atoms per element from a chemical formula string, returning the result as a dictionary. Parsing proceeds right-to-left, which simplifies handling of nested parenthetical groups.

A Reverse Polish Notation calculator implemented as a stack-based processor.

An alternative Reverse Polish Notation parser implementation.

A solution to a variant of the travelling salesman problem that admits a quadratic-complexity algorithm. Originally encountered in a competitive programming context.

A reusable Selenium scraping template that extracts participant website links.