Abstract: 
In this work, we define the Catalan numbers C_{n}
and prove several equivalent definitions (including some closedform
formulae). We also show one of their applications (counting the number
of binary trees of size n), prove the asymptotic growth
approximation C_{n} ∼ 4^{n} / (√π ·
n^{1.5}), and provide reasonably efficient executable
code to compute them. The derivation of the closedform
formulae uses algebraic manipulations of the ordinary generating
function of the Catalan numbers, and the asymptotic approximation is
then done using generalised binomial coefficients and the Gamma
function. Thanks to these highly nonelementary mathematical tools,
the proofs are very short and simple. 
BibTeX: 
@article{Catalan_NumbersAFP,
author = {Manuel Eberl},
title = {Catalan Numbers},
journal = {Archive of Formal Proofs},
month = jun,
year = 2016,
note = {\url{https://isaafp.org/entries/Catalan_Numbers.html},
Formal proof development},
ISSN = {2150914x},
}
