“Iknowonething:Iknownothing”

— Socrates

Projects

God, Substance, and Necessity: Formalizing Spinoza's Ethics in Lean 4

Machine-checked formalization of Spinoza's Ethics Part I using Lean 4 and Mathlib.

Lean4MathlibFormal VerificationPhilosophy

Acoustic Guitar Physical Simulation

Full acoustic chain: 1D string FEM, 2D Kirchhoff-Love soundboard, 3D Yee grid air radiation with PML.

PythonNumPySciPyGetFEMGmshFEM

Sea Ice Drift Estimation: MCC vs CMCC

Cross-correlation methods for Arctic sea ice drift from satellite imagery, validated against IABP buoy tracks.

RustPythonAMSR2 dataASCAT data

GMT — Generic Maths Tool

Scientific computing library: Gaussian process regression, tension splines, ridge regression, Monte Carlo simulation, and neural networks.

PythonNumPySciPyMachine LearningGP Regression

Optimal Texas Hold'em Strategy Laboratory

Texas Hold'em engine with Monte Carlo simulation, formal Lean4 proofs, and RL agents.

PythonLean4Monte CarloReinforcement LearningMachine Learning

Glass Cutting Optimization — ROADEF 2018

6th place out of 64 teams in the ROADEF/EURO 2018 industrial optimization challenge by Saint-Gobain.

C++OpenMPGenetic/EvolutionnarySimulated AnnealingHeuristics

CTU-Solver — Constraint & Integer Programming in Rust

A Rust library combining Constraint Programming (CP) and Integer Programming (IP) with 33+ constraint types, AC-3 propagation, and a simplex solver.

RustConstraint ProgrammingInteger ProgrammingOptimization

Line-Following Robot with micro:bit

A line-following robot using BBC micro:bit, SparkFun MotoBit, and IR sensors with calibration and state-machine control.

MicroPythonmicro:bitRoboticsI2C

3D Drone Digital Twin in Modelica

Full 3D digital twin of a quadrotor drone using OpenModelica and MSL.

ModelicaOpenModelicaControl SystemsSimulation

Space Altimetry and Continental Hydrology

Multi-level satellite altimetry pipeline: Kalman filtering, kriging, waveform retracking, and multi-mission fusion with Dask.

PythonKrigingKalman FilterSARSatellite Altimetry

CVWeb

This portfolio website — a bilingual, animated CV built with Next.js and Tailwind CSS.

Next.jsTypeScript

“WRITINGshowshowsloppyyourTHINKINGis,

MATHSshowshowsloppyyourWRITINGis,

PROGRAMMINGshowshowsloppyyourMATHis.”

— Leslie Lamport