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,657 papers · 148 categories

Trend · papers per month

count % of corpus

10 results for “Mathlib”

Synthetic Differential Geometry in Leancs.LO

Formalizes synthetic differential geometry in Lean.

problem Formalizing synthetic differential geometry in a proof assistant.

method Formalization of synthetic differential geometry with Lean and mathlib.

result Proves a Taylor theorem for functions of several variables.

synthetic differential geometry Lean proof assistant mathlib Taylor theorem constructive mathematics

2026-03-18abs ↗pdf ↗

Elements of Differential Geometry in Lean: A Report for Mathematicianscs.LO

Report on formalizing differential geometry in Lean.

problem Formalizing differential geometry in a proof assistant.

method Lean's type theory approach to formalization.

result Surprising differences between formal and informal proofs.

differential geometry Lean mathlib formalization type theory

2021-08-01abs ↗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 ↗

Towards Formalizing Reinforcement Learning Theorycs.LG

This paper formalizes $Q$ -learning and linear TD convergence using Lean 4.

problem Formalizing convergence properties of

Q

-learning and linear TD learning.

method Formal verification using Lean 4 theorem prover and Mathlib library.

result Formalized almost sure convergence of

Q

-learning and linear TD learning.

Reinforcement Learning Temporal Difference Learning Formal Verification Lean 4 Mathlib

2025-11-05abs ↗pdf ↗

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 ↗

Integral Curves and Flows on Banach Manifolds in Leanmath.DG

Formalizes integral curves on Banach manifolds in Lean.

problem Existence and uniqueness of integral curves on Banach manifolds.

method Formalized differential equations on Banach spaces, then generalized to Banach manifolds.

result Established theorems for integral curves on Banach manifolds.

Banach manifolds integral curves differential equations Picard-Lindelöf theorem Grönwall inequality

2026-02-02abs ↗pdf ↗

Parity of

k

-differentials in genus zero and onemath.NT

Researchers solved a number-theoretic hypothesis to determine the spin parity of k-differentials.

problem Determining the spin parity of k-differentials on Riemann surfaces of genus zero and one.

method Proved a number-theoretic hypothesis (Conjecture A.10) by reformulating it in terms of Jacobi symbols and reducing it to a combinatorial identity.

result The spin parity of k-differentials on Riemann surfaces of genus zero and one was completely determined.

Riemann surfaces k-differentials spin parity number-theoretic hypothesis Jacobi symbols

2026-02-03abs ↗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 ↗

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 ↗