1 citations · 1 across the 5 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2023
Engel's theorem in Mathlib
Oliver Nash
We discuss the theory of Lie algebras in Lean's Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel's theorem and an application to root sp…
cs.LO2023
A formalisation of Gallagher's ergodic theorem
Oliver Nash
Gallagher's ergodic theorem is a result in metric number theory. It states that the approximation of real numbers by rational numbers obeys a striking 'all or nothing' behaviour. W…
cs.LO2022★ 1 cited
Formalising the -principle and sphere eversion
Patrick Massot, Floris van Doorn, Oliver Nash
In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existen…