I am thinking of projects like unimath, mathlib or mathcomp. "Biggest" to be defined in terms of number of theorems from the 1000+ theorems project that have been formally proven in the library.