Skip to content
View alejandro-soto-franco's full-sized avatar
♻️
Riemannianing your geometry
♻️
Riemannianing your geometry

Block or report alejandro-soto-franco

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse

Alejandro Soto Franco

Rust + Math. Founding Principal at Holonomy Securities, where a three-person team ships systematic trading engines (Polybius, Malliavin, Bismut, Hsu) on a shared platform substrate (Colosseum, just launched). Polybius, our Polymarket-native binary options engine, is up roughly 81% since going live.

BS/MSE Biomedical Engineering, Johns Hopkins University. Previously a trading strategies developer at Anti Capital (New York), building multi-exchange async execution systems in Rust.

In parallel I maintain open-source Rust libraries for geometric computing and stochastic analysis (cartan, pathwise, volterra, elworthy), and collaborate with the University of Pittsburgh School of Medicine on applying mermin's topological-defect pipeline to human vaginal fibroblast microscopy.

Website

Open source

Repository Language What it does CI
cartan Rust + Python Riemannian geometry, Lie-group optimisation, and stochastic analysis on manifolds CI
volterra Rust + Python Covariant active-nematics solver via discrete exterior calculus CI
pathwise Rust + Python Simulation and calibration of non-Markovian stochastic differential equations CI
elworthy Rust + Python JIT compiler specialising Bismut-Elworthy-Li Greeks into SIMD kernels CI
hurst Rust Rough volatility on the correlation manifold; Hurst estimation on SPD(N) CI
vonkarman Rust Pseudospectral DNS for the 3D incompressible Navier-Stokes equations CI
gpufft Rust Unified GPU FFT: VkFFT on Vulkan, cuFFT on CUDA CI
ferrum-gpu Rust + Python Pure-Rust GPU compute: Rust-to-PTX FFT kernels with Python bindings CI
spirv-oxide Rust Rust-to-SPIR-V GPU compiler via Pliron MLIR CI
ermak Rust + Python GPU Brownian dynamics for ligand dissociation kinetics CI
inferCNAsc Rust + Python Copy-number alteration inference from single-cell RNA-seq CI
mermin Rust + Python k-atic alignment analysis of fluorescence microscopy CI
tikhonov Rust Pure-Rust Harmony2 for single-cell data integration CI
collint Rust + Python Detect and auto-fix visual collisions in matplotlib figures CI
kloeden C++ + Rust Hand-SIMD C++ versus Rust SDE-scheme benchmark companion CI
rotorlab Rust Geometric-algebra maths-animation engine, rendered via Vulkan CI
vigild Rust Multi-host Linux service-health daemon CI
navier-stokes Python + Lean 3D Navier-Stokes regularity: Lean, numerics, and theory CI
Meridian Lean 4 Metaprogramming toolkit: sorry inventory, proof search, dependency graphs CI
meridian-vscode TypeScript VS Code companion: interactive dependency graph and Mathlib symbol index CI

Research and formalisation

Three-track architecture (Lean 4 + LaTeX + SymPy / Cadabra2) with chapter-level synchronisation between formal, narrative, and symbolic verification. The public Navier-Stokes track is in the table above; the items below are private or pre-release.

Project Language Description
elliptic-dirichlet (private) Lean 4 Machine-verified existence and uniqueness of the weak $H_0^1$ solution of the Dirichlet problem for a uniformly elliptic, divergence-form operator, via Lax-Milgram. Joint formalisation with Kobe Marshall-Stevens.
mars-lnp (private) Rust Defect-mediated hydrodynamic transfer of orientational order in coupled active-lyotropic nematic systems. Simulations on volterra, defect detection via cartan holonomy.

Upstream contributions

Date Project Description Reference
14 Apr 2026 Mathlib4 HasCompactMulSupport closure under product operations: submonoid, List, Multiset, and Finset variants, with @[to_additive]. #38022 · 2ff8885
12 May 2026 cuda-oxide fix(codegen): convert three silent miscompiles in the Rust-to-PTX code generator into hard build errors, including the invalid .version emitted for compute_* targets that ptxas rejects only at JIT time. #27 · 3697238

Quantitative Finance

Private repositories under Holonomy Securities.

Project Description
Colosseum Multi-asset quantitative backtesting platform. WASM strategy sandbox, CLOB-native data, configurable fill models, full audit trail. Rust engine + axum API + Next.js frontend.
Polybius Binary options engine for prediction markets. Non-stationary SDE models, Kelly sizing, CLOB execution. Polymarket live, Kalshi planned. 16-crate workspace.
Malliavin Regime-conditional equity options engine. Directional spreads + vol selling on QQQ. Polygon + CBOE data, Deribit/IBKR venue integrations.
Bismut Volatility surface curvature signals. SSVI fitting, Riemannian curvature extraction, walk-forward backtesting with butterfly and straddle strategies.
Hsu Manifold-valued covariance research engine. Realised covariance matrices as points on SPD(N) with affine-invariant metrics, tangent-space MLE calibration. Built on cartan and pathwise.

Pinned Loading

  1. cartan cartan Public

    Rust crate for Riemannian optimization.

    Rust 1

  2. volterra volterra Public

    Covariant active nematics solver on simplicial meshes.

    Rust 1

  3. Meridian Meridian Public

    Lean 4 metaprogramming toolkit for mathematical formalisation. Sorry inventory with Mathlib DiscrTree coverage, dependency graphs, and IDA* proof search.

    Lean

  4. pathwise pathwise Public

    A composable toolkit for simulation and calibration of non-Markovian stochastic differential equations.

    Rust