A can’t miss awesome thing for people on the precipice of the dependent type theory rabbit hole is 1lab: https://1lab.dev/#lab

1lab is the future for mathematics research that deserves to happen.