/*.lean directly - method: machine autoformalization (two-stage; scout, not author) models: - labs-leanstral-1-5 - magistral-medium framework: "mathfin-foundry: probe / vibe <-> lean-lsp-mcp" tool_setup: token-paced GitHub Actions pipeline; Magistral and an unnamed drafter specify the statement, Leanstral formalizes + proves it. A cheap autop tactic-probe may scout-close a goal Leanstral missed; those open as DRAFT PRs (labeled scout-proof, attributed to the tactic, refactored before merge, never silently merged). On a Leanstral pass it opens a ready-for-review PR on formal-mathfin that a human reviews (8-lens values panel) and merges prompting_notes: "4 autoformalized proof(s) merged (two-stage: statement specified by Magistral (2) and an unnamed drafter (2), formalization + proof by Leanstral) (closing #66, #85, #161, #162)" - method: own design, external source consulted (cited) models: [] framework: Lean 4 + Mathlib, this library's conventions; an Isabelle/HOL AFP entry consulted as a source for the classical result set tool_setup: provenance.source == afp-actuarial-mathematics; per-file citation header; cited with the author's permission prompting_notes: "2 proof(s) authored in our own design, with Yosuke Ito's AFP 'Actuarial Mathematics' (Survival_Model, BSD) consulted as a source and cited (issues #112)" spend_usd: 0 (Mistral Labs beta) notes: "scout, not author: the pipeline opens the PR; a human reviews and merges, so no machine proof enters the library unreviewed" fidelity: divergences: 13 reduced-core (a faithful but reduced formal core of the informal statement) and 18 library-wrappers (a thin restatement consuming a Mathlib/BrownianMotion lemma); 0 placeholders. The reduced-core entries are the honest divergences — each is itemised in docs/coverage.md. review: status: continuous — an 8-lens values-review panel runs at each proof-content change (docs/values-review.md); cadence machine-enforced by test_values_review_is_current reviewers: - Raphael Coelho notes: the review is an upgrade engine (ranked backlog), not a pass/fail gate alignment: namespace: MathFin statements: - source: brownian_motion (Saporito, Stochastic Processes) lean: 10 statements module: benchmarks/brownian_motion.json status: full 4 · wrapper 3 · reduced 3 · placeholder 0 note: per-statement map in docs/coverage.md - source: measure_theory (Saporito, Stochastic Processes) lean: 5 statements module: benchmarks/conditional_expectation.json status: full 0 · wrapper 5 · reduced 0 · placeholder 0 note: per-statement map in docs/coverage.md - source: martingales (Saporito, Stochastic Processes) lean: 4 statements module: benchmarks/continuous_martingales.json status: full 2 · wrapper 2 · reduced 0 · placeholder 0 note: per-statement map in docs/coverage.md - source: measure_theory (Saporito, Stochastic Processes) lean: 3 statements module: benchmarks/cross_validated.json status: full 1 · wrapper 2 · reduced 0 · placeholder 0 note: per-statement map in docs/coverage.md - source: measure_theory (Saporito, Stochastic Processes) lean: 6 statements module: benchmarks/distributions.json status: full 4 · wrapper 2 · reduced 0 · placeholder 0 note: per-statement map in docs/coverage.md - source: stochastic_calculus (Saporito, Stochastic Processes) lean: 18 statements module: benchmarks/girsanov_finance.json status: full 17 · wrapper 0 · reduced 1 · placeholder 0 note: per-statement map in docs/coverage.md - source: markov_chains (Saporito, Stochastic Processes) lean: 9 statements module: benchmarks/markov_chains.json status: full 4 · wrapper 0 · reduced 5 · placeholder 0 note: per-statement map in docs/coverage.md - source: martingales (Saporito, Stochastic Processes) lean: 9 statements module: benchmarks/martingales.json status: full 6 · wrapper 3 · reduced 0 · placeholder 0 note: per-statement map in docs/coverage.md - source: mathematical_finance (Saporito, Stochastic Processes) lean: 243 statements module: benchmarks/mathematical_finance.json status: full 242 · wrapper 1 · reduced 0 · placeholder 0 note: per-statement map in docs/coverage.md - source: poisson_processes (Saporito, Stochastic Processes) lean: 5 statements module: benchmarks/poisson_processes.json status: full 4 · wrapper 0 · reduced 1 · placeholder 0 note: per-statement map in docs/coverage.md - source: stochastic_calculus (Saporito, Stochastic Processes) lean: 41 statements module: benchmarks/stochastic_calculus.json status: full 38 · wrapper 0 · reduced 3 · placeholder 0 note: per-statement map in docs/coverage.md acknowledgements: ""