On-device research index

arXiv research

A locally-built, LLM-digested index of recent arXiv papers in quant finance, geometry/topology, and statistical ML — keyword search served straight from SQLite on this machine.

168,695 papers · 148 categories

Trend · papers per month

count % of corpus

10 results for “machine-checked”

A Machine-Checked Itô Calculus for Brownian Motionq-fin.MF

A machine-checked Itô calculus for Brownian motion on $[0,T]$

problem Developing an

L^2

Itô calculus for Brownian motion

method Formalized in Lean 4 on top of Mathlib and the BrownianMotion package

result First machine-checked proof of Itô's formula and construction of Itô integral as martingale-valued process

Itô calculus Brownian motion machine-checked L^2 Lean

2026-06-13abs ↗pdf ↗

A Machine-Checked Itô Calculus for Brownian Motionq-fin.MF

Developed a machine-checked Itô calculus for Brownian motion.

problem Formal verification of Itô calculus for Brownian motion.

method Machine-checked formalization in Lean over Mathlib.

result First machine-checked constructions of the Itô integral and Itô's formula.

Itô calculus Brownian motion machine-checked proof assistant Leibniz integral rule

2026-06-13abs ↗pdf ↗

The Fundamental Theorem of Asset Pricing, Formalized in Lean 4q-fin.MF

Formalizes the Fundamental Theorem of Asset Pricing in Lean 4.

problem Formalizing the Fundamental Theorem of Asset Pricing in a proof assistant.

method Formalization in Lean 4 over Mathlib, covering three market settings.

result Constructs the equivalent martingale measure explicitly and proves its properties.

Fundamental Theorem of Asset Pricing Lean 4 Mathlib Machine-checked Arbitrage

2026-06-27abs ↗pdf ↗

Quantifying Bounded Rationality: Formal Verification of Simon's Satisficing Through Flexible Stochastic Dominanceq-fin.MF

Paper formalizes Simon's satisficing through FFSD, proving its equivalence to expected utility theory.

problem Formalizing Herbert Simon's bounded rationality concept in economic decision-making.

method Developed FFSD framework using Lean 4 theorem prover, proving equivalence to expected utility theory.

result Equivalence theorem linking FFSD to expected utility maximization for approximate indicator functions.

Simon's satisficing FFSD expected utility theory Lean 4 bounded rationality

2025-07-02abs ↗pdf ↗

Verification of ML Systems via Reparameterizationcs.LG

This research simplifies verification of machine learning systems using reparameterization.

problem Reduce or eliminate serious bugs in machine learning systems.

method Use proof assistants to construct machine-checked proofs of correctness, leveraging reparameterization to handle probabilistic claims.

result Demonstrates broad applicability of reparameterization to verify different types of machine learning systems.

machine learning verification reparameterization proof assistants PAC-learnability

2020-07-14abs ↗pdf ↗

A Formally Verified Library of Mathematical Finance in Lean 4q-fin.MF

Lean 4 library formalizes mathematical finance, verifying over 200 theorems.

problem Formal verification of complex financial mathematics.

method Lean 4 proof assistant, Mathlib, BrownianMotion package, formal verification of over 200 theorems.

result Formal verification yields certified unification of known financial results.

mathematical finance formal verification Lean 4 stochastic calculus risk-neutral pricing

2026-05-31abs ↗pdf ↗

A Formally Verified Library of Mathematical Finance in Lean 4q-fin.MF

Lean 4 library formalizes mathematical finance, verifying over 200 theorems.

problem Formal verification of complex financial mathematics.

method Lean 4 proof assistant, Mathlib, and BrownianMotion package.

result Formal verification yields certified unification of known results.

mathematical finance formal verification Lean 4 stochastic calculus risk-neutral pricing

2026-05-31abs ↗pdf ↗

Exponential Family Discriminant Analysis: Generalizing LDA-Style Generative Classification to Non-Gaussian Modelscs.LG

EFDA extends LDA to non-Gaussian models using exponential families.

problem Classifying non-Gaussian data with LDA's limitations.

method EFDA uses exponential families to derive closed-form estimators for natural parameters and a linear decision rule.

result EFDA matches LDA's accuracy while reducing ECE by 2-6x, proving asymptotic calibration and efficiency.

Exponential Family Discriminant Analysis LDA Non-Gaussian Models Exponential Family Maximum Likelihood Estimation

2026-03-21abs ↗pdf ↗

Budget-Sensitive Discovery Scoring: A Formally Verified Framework for Evaluating AI-Guided Scientific Selectioncs.LG

Framework evaluates AI proposals for drug discovery, finds no LLM advantage.

problem No principled framework exists for evaluating AI-guided scientific selection under budget constraints.

method Formally verified metric (BSDS/DQS) penalizes false discoveries and excessive abstention.

result LLMs provide no marginal value over existing classifiers in drug discovery.

AI scientific selection budget constraints formally verified discovery quality score

2026-03-12abs ↗pdf ↗

A Formal Approach to AMM Fee Mechanisms with Lean 4q-fin.MF

We introduce trading fees into AMM models and analyze their impact on swap rates and profits.

problem The impact of trading fees on AMM models and users' trading strategies.

method We extend a foundational AMM model by introducing a trading fee parameter and analyze the model using economic and mathematical rigor.

result Trading fees affect the additivity of swap rates and can lead to greater profits from larger trades.

AMM models trading fees automated market makers Lean 4 economic analysis

2026-01-24abs ↗pdf ↗