Stochastic analysis and numerical methods: McKean–Vlasov forward–backward SDEs with jumps, their well-posedness, a posteriori error estimates for their solvers, and Lean 4 formalisations of the results. MEng Electronic Engineering and MSc Scientific Computing, Durham University.
Research
- Well-posedness of fully coupled McKean–Vlasov FBSDEs with jumps under full-tuple law dependence, with C. Feng. arXiv:2608.23203, with its Lean formalisation in mvfbsdej-well-posedness-lean.
- LevyStochCalc: a Lean 4 + Mathlib library of Lévy-driven stochastic calculus (Itô and Poisson integrals, the Itô–Lévy formula, BSDEs with jumps).
Tools
- MachineChecked: read a mathematical paper beside its Lean formalisation, claim by claim. Site: machinechecked.org.
- papercheck: a reproducible audit harness for mathematical LaTeX papers.
- Ariadne: an MCP server for running a literature review.
Hardware
- deepJFET: an Intel 4004 built from silicon-carbide JFET logic and simulated at transistor level.
- advent-of-camel-2025: Advent of Code 2025 as cycle-accurate FPGA designs in Hardcaml.
christiangarry.com · LinkedIn · christian@christiangarry.com