Research
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
0.3%0.5%0.8%0.1% · Jun 202619922001200920172026
2 results for “mathlib4”
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0cs.LO

Lean 4 formalizes Stokes' theorem for smooth singular cubes.

problem Formalizing Stokes' theorem for singular cubes in arbitrary dimensions.
method Using true differential-form pullback via Frechet derivative, bridging to mathlib4's extDeriv.
result d^2=0 for singular cubical chains, chain-level Stokes extended.
Stokes' theoremsmooth singular cubesFrechet derivativemathlib4differential forms
2026-05-01abs ↗pdf ↗