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.
A new version of MarkdowntoLaTeX is currently under development. Switch to the dev branch to follow its progress.
Functional Analysis ⭐ 16
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.
Bellingcat ⭐ 11
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.