Quantitative Research · Statistical Analysis · Mathematical Modelling · Econometrics · Causal Inference · Forecasting · Optimization · AI Evaluation
I work on quantitative problems where obtaining a coefficient, forecast, probability, optimum, or benchmark answer is only the beginning. My projects make assumptions explicit, separate identification from estimation, test failure modes, independently validate critical outputs, and limit conclusions to what the design actually supports.
How do identification assumptions fail in DiD, IV, RD and matching designs?
When is a fluent quantitative answer still invalid as economics or econometrics?
Can a candidate solution be checked by an independent calculation rather than by repeating the same code path?
Which inferential claims survive a known data-generating process?
→ docs/statistical_error_catalogue.md
Does a reported optimum satisfy the programme that was actually written down?
When is a forecast validated, rather than merely well fitted in sample?
→ FORECAST_VALIDATION_PLAYBOOK.md
Samples in the Python laboratories are documented simulated DGPs (or closed forms). That is the design: the true ATT, break date, coverage probability, or optimum is known, so a wrong procedure can be shown to fail. They are not observational extracts, and recovering a simulated parameter is not an empirical finding.
The YAML evaluation corpus is coded by one author. Cohen's kappa in that repository is arithmetic on known label tables, not a second-rater study (issue #5).
Identification, scoring, and validation write-ups sit in the repositories above. Three further notes are useful when the question is leakage, serving parity, or information-set integrity rather than an estimand:
- CASE_STUDY_MODEL_SELECTION_FAILURE.md — invalid selection workflows versus the matching split
- FLAGSHIP_POINT_IN_TIME_FAILURE.md — features that use post-cutoff events
- FLAGSHIP_TRAINING_SERVING_SKEW.md — a live endpoint whose number is not the fitted pipeline
Supporting laboratories, not a second identity:
| Repository | Question |
|---|---|
| quantitative-finance-models | Which valuation and risk identities hold on closed forms or simulated series? |
| machine-learning-model-selection-lab | What risk does a given validation design actually estimate? |
| genai-rag-evaluation-lab | Can retrieval failure be separated from generation failure? |
| pytorch-deep-learning-lab | Do hand derivatives, finite differences, and autograd agree away from kinks? |
| sql-ml-feature-engineering-lab | Does a feature use only information available at the cutoff? |
| mlops-reproducible-serving-lab | Does serving reproduce the training-pipeline prediction on the same valid input? |
These are research programmes with tests and CI. They are not production systems, trading books, or client deployments.
How can a mathematical statement be translated, proved, reviewed, and repaired in Lean without losing its intended meaning?
Compilation is not faithfulness. Lean is used here for explicit domains, quantifiers, existence versus uniqueness, and boundary cases. A compiled theorem does not establish an empirical causal claim.
Each Lean repository is a released case library: the theorems were published together in the initial commit. That is a catalogue release, not a missing commit diary. Where a later commit exists, it is a documentation or link correction. CI checks that lake build (or the documented test) still runs.
The libraries are listed from economic modelling toward classical analysis:
Feasible sets, budget constraints, inequalities, and theorem-level checks of optimisation claims used in mathematical economics.
An executable review library of semantic errors that can survive compilation: omitted hypotheses, quantifier mistakes, and repairs that keep the intended statement.
Hidden assumptions, domain restrictions, weakening versus strengthening, and the distinction between a valid proof of the wrong claim and a faithful formalization.
Structured construction, rewriting, induction, and decomposition so that assumptions and failure modes remain readable.
Continuity versus uniform continuity, pointwise versus uniform convergence, compactness, and domain conditions that over-generalized statements omit.
Why a tactic succeeds or fails, and whether the resulting theorem still expresses the intended mathematics.
Rolle, Lagrange, and Cauchy reconstructed from the extreme value theorem and Fermat’s lemma rather than quoted as mathlib one-liners.
Unfinished bounds in the Python laboratories are listed in each lab’s ROADMAP.md. GitHub issues are used where a remaining gap is still unimplemented. The evaluation corpus has no second human rater (issue #5). nDCG in the RAG laboratory is binary, not graded. The econometrics wild-cluster interval is a Rademacher percentile of coefficients, not Webb weights or a restricted bootstrap-t.
The Lean repositories are released case libraries. Unfinished mathematics is in each README's limitation notes, not in a fake commit diary. lake build does not certify an observational application.
Python · R · SQL · statsmodels · scikit-learn · SciPy · PyTorch · Git/GitHub · Lean 4/mathlib