In this project, conducted by the Barcelona LEAN Seminar, we have started a formalization of the Brouwer Fixed Point, following the paper "Hi havia una vegada un punt fix..." writen by Dr Natalia Castellana (from UAB).

Because we are formalization a complex proof we have created a Blueprint to follow conceptually what we are doing in code, this blueprint can be found here. You can also see the GitHub repository here.