Mathematical engineer. Deep interest formal methods. Below is a selection of projects, active and completed.
Functional Analysis ⭐ 17
Selected solutions to Rudin's Functional Analysis. Ongoing revision and expansion. You can download them as a pdf file.
SKILL.md files for Claude.
| Skill | Purpose |
|---|---|
| grammar | Rules for using and punctuating "so", "thus", "therefore", "hence" in English. |
| latex-formatting | Format LuaLaTeX .tex files (line length, indentation, comments, end of file). |
| mathematical-writing | Rule graph for writing, refereeing and polishing mathematics (after Knuth, Halmos et al.). |
| proofreading | Proofread LuaLaTeX math books (American English); findings go to review.md. |
| python-programming | Create/update Python code and documentation following best practices. |
| web-app | Build web apps, scoped to your <OUTPUT_DIR> folder. |
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.
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.