Formalization Project for Logika v Računalništvu

This project involves the formalization of Catalan numbers and related combinatorial structures. All tasks are available in the main.lean file.

Completed Tasks

Small Tasks

1. Recursive Definition of Catalan Numbers
2. Formalization of Plane Trees
3. Formalization of Full Binary Trees
4. Enumeration of Full Binary Trees with n Nodes
5. Generation of Ballot Sequences of Length n

Large Tasks

1. Bijection between List Plane Trees and Plane Trees
2. Rotation Isomorphism in Trees
3. Proof that $\binom{2n}{n}$ is Divisible by $n+1$ (partial proof)
4. Proof that $C_n = \frac{\binom{2n}{n}}{n+1}$