I built a toy autonomous math research project: https://paulklemstine.github.io/Lean/