- The uncountability of ℝ
- The reals axioms imply Markov principle
- Basel problem (
*1+1/2²+1/3²+1/4²+...= π²/6*) - Stirling Formula (approximation for
*n!*) - Lagrange's four-square theorem

- Arithmetic
- Topology (Various typeclasses definitions)
- Clean libraries on sequences of reals or complexes
- Complexes' definition and collection of basic results
- Formalization of power series and their convergence radius