Open Issues Need Help
View All on GitHub Worked example: suspension flow of a smooth Anosov base carrying its OWN derivative-cocycle flow Lyapunov exponent (λ_flow = λ_base/∫τ) about 4 hours ago
enhancement help wanted
A Lean 4 + Mathlib formalization of the Oseledets multiplicative ergodic theorem (MET), with a leanblueprint and doc-gen4 documentation.
Lean
#ergodic-theory#formal-methods#formalization#lean#lean4#lyapunov-exponents#mathematics#mathlib
Livšic cohomology: coboundary ⇔ vanishing periodic-orbit sums (non-entropic no-section obstruction for hyperbolic systems) about 4 hours ago
enhancement help wanted
A Lean 4 + Mathlib formalization of the Oseledets multiplicative ergodic theorem (MET), with a leanblueprint and doc-gen4 documentation.
Lean
#ergodic-theory#formal-methods#formalization#lean#lean4#lyapunov-exponents#mathematics#mathlib